Theorem imor 867

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  imori  868  imorri  869  pm4.62  870  pm4.78  948  pm4.52  1000  dfifp4  1082  dfifp5  1083  dfifp7  1085  norasslem1  1564  rb-bijust  1782  rb-imdf  1783  rb-ax1  1785  nf2  1818  relsnb  5780  soxp  8130  modom  9226  dffin7-2  10457  algcvgblem  16732  divgcdodd  16866  flt4lem7  27971  nna4b4nsq  27972  noinfprefixmo  28040  chrelat2i  32949  disjex  33168  disjexc  33169  meran1  37169  meran3  37171  bj-dfbi5  37414  bj-andnotim  37428  itg2addnclem2  38558  dvasin  38590  impor  38983  biimpor  38986  moeu2  39270  hlrelat2  40428  sticksstones1  43164  ifpim1  44428  ifpim2  44431  ifpidg  44450  ifpim23g  44454  ifpim123g  44459  ifpimimb  44463  ifpororb  44464  sqrtcvallem1  44590  hbimpgVD  45845  stoweidlem14  46968  fvmptrabdm  48307  fullthinc  50502  alimp-surprise  50820  eximp-surprise  50824