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  1535  rb-bijust  1750  rb-imdf  1751  rb-ax1  1753  nf2  1786  relsnb  5751  soxp  8071  modom  9151  dffin7-2  10308  algcvgblem  16504  divgcdodd  16637  noinfprefixmo  27669  chrelat2i  32440  disjex  32667  disjexc  32668  meran1  36605  meran3  36607  bj-dfbi5  36774  bj-andnotim  36788  itg2addnclem2  37869  dvasin  37901  impor  38278  biimpor  38281  moeu2  38551  hlrelat2  39659  sticksstones1  42396  flt4lem7  42898  nna4b4nsq  42899  ifpim1  43706  ifpim2  43709  ifpidg  43728  ifpim23g  43732  ifpim123g  43737  ifpimimb  43741  ifpororb  43742  sqrtcvallem1  43868  hbimpgVD  45140  stoweidlem14  46254  fvmptrabdm  47535  fullthinc  49691  alimp-surprise  50021  eximp-surprise  50025