Theorem imor 867

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  imori  868  imorri  869  pm4.62  870  pm4.78  948  pm4.52  1000  dfifp4  1082  dfifp5  1083  dfifp7  1085  norasslem1  1563  rb-bijust  1781  rb-imdf  1782  rb-ax1  1784  nf2  1817  relsnb  5779  soxp  8143  modom  9245  dffin7-2  10479  algcvgblem  16757  divgcdodd  16891  flt4lem7  27994  nna4b4nsq  27995  noinfprefixmo  28063  chrelat2i  32972  disjex  33233  disjexc  33234  meran1  37291  meran3  37293  bj-dfbi5  37536  bj-andnotim  37550  itg2addnclem2  38683  dvasin  38715  impor  39108  biimpor  39111  moeu2  39395  hlrelat2  40553  sticksstones1  43289  ifpim1  44563  ifpim2  44566  ifpidg  44585  ifpim23g  44589  ifpim123g  44594  ifpimimb  44598  ifpororb  44599  sqrtcvallem1  44724  hbimpgVD  45979  stoweidlem14  47117  fvmptrabdm  48456  fullthinc  50678  alimp-surprise  51044  eximp-surprise  51048