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  5785  soxp  8168  modom  9270  dffin7-2  10503  algcvgblem  16781  divgcdodd  16915  flt4lem7  28019  nna4b4nsq  28020  noinfprefixmo  28088  chrelat2i  32997  disjex  33258  disjexc  33259  mirimanofffr  36629  meran1  37377  meran3  37379  bj-dfbi5  37622  bj-andnotim  37636  itg2addnclem2  38782  dvasin  38814  impor  39207  biimpor  39210  moeu2  39494  hlrelat2  40652  sticksstones1  43388  ifpim1  44662  ifpim2  44665  ifpidg  44684  ifpim23g  44688  ifpim123g  44693  ifpimimb  44697  ifpororb  44698  sqrtcvallem1  44823  hbimpgVD  46077  stoweidlem14  47229  fvmptrabdm  48568  fullthinc  50790  alimp-surprise  51156  eximp-surprise  51160