Theorem imor 849

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

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

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 844

This theorem is referenced by:  imori  850  imorri  851  pm4.62  852  pm4.78  931  pm4.52  981  dfifp4  1061  dfifp5  1062  dfifp7  1064  norasslem1  1529  rb-bijust  1749  rb-imdf  1750  rb-ax1  1752  nf2  1785  r19.30OLD  3342  relsnb  5678  soxp  7826  modom  8722  dffin7-2  9823  algcvgblem  15924  divgcdodd  16057  chrelat2i  30145  disjex  30345  disjexc  30346  meran1  33763  meran3  33765  bj-dfbi5  33911  bj-andnotim  33926  itg2addnclem2  34948  dvasin  34982  impor  35363  biimpor  35366  hlrelat2  36543  ifpim1  39840  ifpim2  39843  ifpidg  39863  ifpim23g  39867  ifpim123g  39872  ifpimimb  39876  ifpororb  39877  hbimpgVD  41244  stoweidlem14  42306  fvmptrabdm  43499  alimp-surprise  44888  eximp-surprise  44892