Theorem imor 850

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  imori  851  imorri  852  pm4.62  853  pm4.78  932  pm4.52  982  dfifp4  1064  dfifp5  1065  dfifp7  1067  norasslem1  1532  rb-bijust  1752  rb-imdf  1753  rb-ax1  1755  nf2  1788  relsnb  5712  soxp  7970  modom  9023  dffin7-2  10154  algcvgblem  16282  divgcdodd  16415  chrelat2i  30727  disjex  30931  disjexc  30932  noinfprefixmo  33904  meran1  34600  meran3  34602  bj-dfbi5  34755  bj-andnotim  34770  itg2addnclem2  35829  dvasin  35861  impor  36239  biimpor  36242  hlrelat2  37417  sticksstones1  40102  flt4lem7  40496  nna4b4nsq  40497  ifpim1  41076  ifpim2  41079  ifpidg  41098  ifpim23g  41102  ifpim123g  41107  ifpimimb  41111  ifpororb  41112  sqrtcvallem1  41239  hbimpgVD  42524  stoweidlem14  43555  fvmptrabdm  44785  fullthinc  46327  alimp-surprise  46484  eximp-surprise  46488