Theorem imor 864

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 317	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 351	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 859	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 280	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ wo 858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-or 859

This theorem is referenced by:  imori  865  imorri  866  pm4.62  867  pm4.78  945  pm4.52  997  dfifp4  1077  dfifp5  1078  dfifp7  1080  norasslem1  1553  rb-bijust  1768  rb-imdf  1769  rb-ax1  1771  nf2  1804  relsnb  5773  soxp  8104  modom  9191  dffin7-2  10352  algcvgblem  16594  divgcdodd  16728  noinfprefixmo  27742  chrelat2i  32514  disjex  32741  disjexc  32742  meran1  36735  meran3  36737  bj-dfbi5  36981  bj-andnotim  36995  itg2addnclem2  38135  dvasin  38167  impor  38544  biimpor  38547  moeu2  38833  hlrelat2  39991  sticksstones1  42727  flt4lem7  43205  nna4b4nsq  43206  ifpim1  44009  ifpim2  44012  ifpidg  44031  ifpim23g  44035  ifpim123g  44040  ifpimimb  44044  ifpororb  44045  sqrtcvallem1  44171  hbimpgVD  45443  stoweidlem14  46552  fvmptrabdm  47851  fullthinc  50035  alimp-surprise  50365  eximp-surprise  50369