Theorem imor 427

Description: Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.)

Assertion

Ref	Expression
imor	⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Proof of Theorem imor

Step	Hyp	Ref	Expression
1		notnotb 304	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 338	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 384	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 267	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 384

This theorem is referenced by:  imori  428  imorri  429  pm4.62  434  pm4.52  511  pm4.78  605  dfifp4  1036  dfifp5  1037  dfifp7  1039  rb-bijust  1714  rb-imdf  1715  rb-ax1  1717  nf2  1751  r19.30  3111  soxp  7335  modom  8202  dffin7-2  9258  algcvgblem  15337  divgcdodd  15469  chrelat2i  29352  disjex  29531  disjexc  29532  meran1  32535  meran3  32537  bj-dfbi5  32684  bj-andnotim  32698  itg2addnclem2  33592  dvasin  33626  impor  34010  biimpor  34013  hlrelat2  35007  ifpim1  38130  ifpim2  38133  ifpidg  38153  ifpim23g  38157  ifpim123g  38162  ifpimimb  38166  ifpororb  38167  hbimpgVD  39454  stoweidlem14  40549  fvmptrabdm  41632  alimp-surprise  42854  eximp-surprise  42858