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  5794  soxp  8134  modom  9221  dffin7-2  10400  algcvgblem  16660  divgcdodd  16794  noinfprefixmo  27902  chrelat2i  32754  disjex  32974  disjexc  32975  meran1  36963  meran3  36965  bj-dfbi5  37208  bj-andnotim  37222  itg2addnclem2  38364  dvasin  38396  impor  38773  biimpor  38776  moeu2  39060  hlrelat2  40218  sticksstones1  42954  flt4lem7  43432  nna4b4nsq  43433  ifpim1  44236  ifpim2  44239  ifpidg  44258  ifpim23g  44262  ifpim123g  44267  ifpimimb  44271  ifpororb  44272  sqrtcvallem1  44398  hbimpgVD  45653  stoweidlem14  46769  fvmptrabdm  48071  fullthinc  50269  alimp-surprise  50599  eximp-surprise  50603