Theorem imor 854

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 315	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 349	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 849	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 278	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  imori  855  imorri  856  pm4.62  857  pm4.78  935  pm4.52  987  dfifp4  1067  dfifp5  1068  dfifp7  1070  norasslem1  1536  rb-bijust  1751  rb-imdf  1752  rb-ax1  1754  nf2  1787  relsnb  5751  soxp  8072  modom  9154  dffin7-2  10311  algcvgblem  16537  divgcdodd  16671  noinfprefixmo  27679  chrelat2i  32451  disjex  32677  disjexc  32678  meran1  36609  meran3  36611  bj-dfbi5  36855  bj-andnotim  36869  itg2addnclem2  38007  dvasin  38039  impor  38416  biimpor  38419  moeu2  38705  hlrelat2  39863  sticksstones1  42599  flt4lem7  43106  nna4b4nsq  43107  ifpim1  43914  ifpim2  43917  ifpidg  43936  ifpim23g  43940  ifpim123g  43945  ifpimimb  43949  ifpororb  43950  sqrtcvallem1  44076  hbimpgVD  45348  stoweidlem14  46460  fvmptrabdm  47753  fullthinc  49937  alimp-surprise  50267  eximp-surprise  50271