Theorem imor 851

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

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

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 846

This theorem is referenced by:  imori  852  imorri  853  pm4.62  854  pm4.78  933  pm4.52  983  dfifp4  1065  dfifp5  1066  dfifp7  1068  norasslem1  1535  rb-bijust  1751  rb-imdf  1752  rb-ax1  1754  nf2  1787  relsnb  5802  soxp  8117  modom  9246  dffin7-2  10395  algcvgblem  16516  divgcdodd  16649  noinfprefixmo  27211  chrelat2i  31656  disjex  31861  disjexc  31862  meran1  35388  meran3  35390  bj-dfbi5  35543  bj-andnotim  35558  itg2addnclem2  36632  dvasin  36664  impor  37041  biimpor  37044  moeu2  37323  hlrelat2  38366  sticksstones1  41054  flt4lem7  41489  nna4b4nsq  41490  ifpim1  42308  ifpim2  42311  ifpidg  42330  ifpim23g  42334  ifpim123g  42339  ifpimimb  42343  ifpororb  42344  sqrtcvallem1  42470  hbimpgVD  43753  stoweidlem14  44815  fvmptrabdm  46086  fullthinc  47750  alimp-surprise  47911  eximp-surprise  47915