Theorem imor 866

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 861	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 281	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  imori  867  imorri  868  pm4.62  869  pm4.78  947  pm4.52  1000  dfifp4  1082  dfifp5  1083  dfifp7  1085  norasslem1  1564  rb-bijust  1779  rb-imdf  1780  rb-ax1  1782  nf2  1815  relsnb  5791  soxp  8126  modom  9212  dffin7-2  10383  algcvgblem  16636  divgcdodd  16770  noinfprefixmo  27843  chrelat2i  32695  disjex  32915  disjexc  32916  meran1  36900  meran3  36902  bj-dfbi5  37145  bj-andnotim  37159  itg2addnclem2  38301  dvasin  38333  impor  38710  biimpor  38713  moeu2  38997  hlrelat2  40155  sticksstones1  42891  flt4lem7  43371  nna4b4nsq  43372  ifpim1  44175  ifpim2  44178  ifpidg  44197  ifpim23g  44201  ifpim123g  44206  ifpimimb  44210  ifpororb  44211  sqrtcvallem1  44337  hbimpgVD  45592  stoweidlem14  46708  fvmptrabdm  48007  fullthinc  50205  alimp-surprise  50535  eximp-surprise  50539