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  5787  soxp  8131  modom  9225  dffin7-2  10404  algcvgblem  16673  divgcdodd  16807  noinfprefixmo  27945  chrelat2i  32854  disjex  33073  disjexc  33074  meran1  37038  meran3  37040  bj-dfbi5  37283  bj-andnotim  37297  itg2addnclem2  38429  dvasin  38461  impor  38839  biimpor  38842  moeu2  39126  hlrelat2  40284  sticksstones1  43020  flt4lem7  43513  nna4b4nsq  43514  ifpim1  44317  ifpim2  44320  ifpidg  44339  ifpim23g  44343  ifpim123g  44348  ifpimimb  44352  ifpororb  44353  sqrtcvallem1  44479  hbimpgVD  45734  stoweidlem14  46850  fvmptrabdm  48189  fullthinc  50384  alimp-surprise  50717  eximp-surprise  50721