Theorem imor 850

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 318	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 353	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 845	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 281	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  imori  851  imorri  852  pm4.62  853  pm4.78  932  pm4.52  982  dfifp4  1062  dfifp5  1063  dfifp7  1065  norasslem1  1531  rb-bijust  1751  rb-imdf  1752  rb-ax1  1754  nf2  1787  relsnb  5639  soxp  7806  modom  8703  dffin7-2  9809  algcvgblem  15911  divgcdodd  16044  chrelat2i  30148  disjex  30355  disjexc  30356  meran1  33872  meran3  33874  bj-dfbi5  34020  bj-andnotim  34035  itg2addnclem2  35109  dvasin  35141  impor  35519  biimpor  35522  hlrelat2  36699  ifpim1  40177  ifpim2  40180  ifpidg  40199  ifpim23g  40203  ifpim123g  40208  ifpimimb  40212  ifpororb  40213  sqrtcvallem1  40331  hbimpgVD  41610  stoweidlem14  42656  fvmptrabdm  43849  alimp-surprise  45308  eximp-surprise  45312