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  5781  soxp  8128  modom  9252  dffin7-2  10412  algcvgblem  16596  divgcdodd  16729  noinfprefixmo  27665  chrelat2i  32346  disjex  32573  disjexc  32574  meran1  36429  meran3  36431  bj-dfbi5  36592  bj-andnotim  36606  itg2addnclem2  37696  dvasin  37728  impor  38105  biimpor  38108  moeu2  38380  hlrelat2  39422  sticksstones1  42159  flt4lem7  42682  nna4b4nsq  42683  ifpim1  43493  ifpim2  43496  ifpidg  43515  ifpim23g  43519  ifpim123g  43524  ifpimimb  43528  ifpororb  43529  sqrtcvallem1  43655  hbimpgVD  44928  stoweidlem14  46043  fvmptrabdm  47322  fullthinc  49336  alimp-surprise  49644  eximp-surprise  49648