Theorem imor 854

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 849	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 278	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

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

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 849

This theorem is referenced by:  imori  855  imorri  856  pm4.62  857  pm4.78  935  pm4.52  987  dfifp4  1067  dfifp5  1068  dfifp7  1070  norasslem1  1536  rb-bijust  1751  rb-imdf  1752  rb-ax1  1754  nf2  1787  relsnb  5752  soxp  8073  modom  9155  dffin7-2  10312  algcvgblem  16508  divgcdodd  16641  noinfprefixmo  27673  chrelat2i  32423  disjex  32649  disjexc  32650  meran1  36586  meran3  36588  bj-dfbi5  36749  bj-andnotim  36763  itg2addnclem2  37844  dvasin  37876  impor  38253  biimpor  38256  moeu2  38542  hlrelat2  39700  sticksstones1  42437  flt4lem7  42938  nna4b4nsq  42939  ifpim1  43746  ifpim2  43749  ifpidg  43768  ifpim23g  43772  ifpim123g  43777  ifpimimb  43781  ifpororb  43782  sqrtcvallem1  43908  hbimpgVD  45180  stoweidlem14  46294  fvmptrabdm  47575  fullthinc  49731  alimp-surprise  50061  eximp-surprise  50065