Theorem imor 853

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 315	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 349	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 848	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 278	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  imori  854  imorri  855  pm4.62  856  pm4.78  934  pm4.52  986  dfifp4  1066  dfifp5  1067  dfifp7  1069  norasslem1  1534  rb-bijust  1749  rb-imdf  1750  rb-ax1  1752  nf2  1785  relsnb  5768  soxp  8111  modom  9198  dffin7-2  10358  algcvgblem  16554  divgcdodd  16687  noinfprefixmo  27620  chrelat2i  32301  disjex  32528  disjexc  32529  meran1  36406  meran3  36408  bj-dfbi5  36569  bj-andnotim  36583  itg2addnclem2  37673  dvasin  37705  impor  38082  biimpor  38085  moeu2  38351  hlrelat2  39404  sticksstones1  42141  flt4lem7  42654  nna4b4nsq  42655  ifpim1  43465  ifpim2  43468  ifpidg  43487  ifpim23g  43491  ifpim123g  43496  ifpimimb  43500  ifpororb  43501  sqrtcvallem1  43627  hbimpgVD  44900  stoweidlem14  46019  fvmptrabdm  47298  fullthinc  49443  alimp-surprise  49773  eximp-surprise  49777