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  1563  rb-bijust  1781  rb-imdf  1782  rb-ax1  1784  nf2  1817  relsnb  5779  soxp  8141  modom  9243  dffin7-2  10477  algcvgblem  16753  divgcdodd  16887  flt4lem7  27990  nna4b4nsq  27991  noinfprefixmo  28059  chrelat2i  32968  disjex  33229  disjexc  33230  meran1  37242  meran3  37244  bj-dfbi5  37487  bj-andnotim  37501  itg2addnclem2  38634  dvasin  38666  impor  39059  biimpor  39062  moeu2  39346  hlrelat2  40504  sticksstones1  43240  ifpim1  44514  ifpim2  44517  ifpidg  44536  ifpim23g  44540  ifpim123g  44545  ifpimimb  44549  ifpororb  44550  sqrtcvallem1  44675  hbimpgVD  45930  stoweidlem14  47068  fvmptrabdm  48407  fullthinc  50602  alimp-surprise  50920  eximp-surprise  50924