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  5765  soxp  8108  modom  9191  dffin7-2  10351  algcvgblem  16547  divgcdodd  16680  noinfprefixmo  27613  chrelat2i  32294  disjex  32521  disjexc  32522  meran1  36399  meran3  36401  bj-dfbi5  36562  bj-andnotim  36576  itg2addnclem2  37666  dvasin  37698  impor  38075  biimpor  38078  moeu2  38344  hlrelat2  39397  sticksstones1  42134  flt4lem7  42647  nna4b4nsq  42648  ifpim1  43458  ifpim2  43461  ifpidg  43480  ifpim23g  43484  ifpim123g  43489  ifpimimb  43493  ifpororb  43494  sqrtcvallem1  43620  hbimpgVD  44893  stoweidlem14  46012  fvmptrabdm  47294  fullthinc  49439  alimp-surprise  49769  eximp-surprise  49773