Theorem imor 866

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 318	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 352	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 861	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 281	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  imori  867  imorri  868  pm4.62  869  pm4.78  947  pm4.52  1000  dfifp4  1080  dfifp5  1081  dfifp7  1083  norasslem1  1557  rb-bijust  1772  rb-imdf  1773  rb-ax1  1775  nf2  1808  relsnb  5780  soxp  8113  modom  9199  dffin7-2  10370  algcvgblem  16625  divgcdodd  16759  noinfprefixmo  27823  chrelat2i  32626  disjex  32847  disjexc  32848  meran1  36784  meran3  36786  bj-dfbi5  37029  bj-andnotim  37043  itg2addnclem2  38183  dvasin  38215  impor  38592  biimpor  38595  moeu2  38881  hlrelat2  40039  sticksstones1  42775  flt4lem7  43253  nna4b4nsq  43254  ifpim1  44057  ifpim2  44060  ifpidg  44079  ifpim23g  44083  ifpim123g  44088  ifpimimb  44092  ifpororb  44093  sqrtcvallem1  44219  hbimpgVD  45477  stoweidlem14  46586  fvmptrabdm  47885  fullthinc  50079  alimp-surprise  50409  eximp-surprise  50413