Theorem imor 842

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 307	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 341	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 837	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 270	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∨ wo 836

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 199  df-or 837

This theorem is referenced by:  imori  843  imorri  844  pm4.62  845  pm4.78  921  pm4.52  970  dfifp4  1050  dfifp5  1051  dfifp7  1053  rb-bijust  1793  rb-imdf  1794  rb-ax1  1796  nf2  1829  r19.30  3268  relsnb  5475  soxp  7573  modom  8451  dffin7-2  9557  algcvgblem  15700  divgcdodd  15830  chrelat2i  29800  disjex  29972  disjexc  29973  meran1  32997  meran3  32999  bj-dfbi5  33141  bj-andnotim  33156  itg2addnclem2  34092  dvasin  34126  impor  34509  biimpor  34512  hlrelat2  35562  ifpim1  38781  ifpim2  38784  ifpidg  38804  ifpim23g  38808  ifpim123g  38813  ifpimimb  38817  ifpororb  38818  hbimpgVD  40083  stoweidlem14  41168  fvmptrabdm  42344  alimp-surprise  43642  eximp-surprise  43646