Theorem imor 852

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 847	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 278	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

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

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 847

This theorem is referenced by:  imori  853  imorri  854  pm4.62  855  pm4.78  933  pm4.52  983  dfifp4  1065  dfifp5  1066  dfifp7  1068  norasslem1  1528  rb-bijust  1744  rb-imdf  1745  rb-ax1  1747  nf2  1780  relsnb  5798  soxp  8128  modom  9262  dffin7-2  10415  algcvgblem  16541  divgcdodd  16674  noinfprefixmo  27627  chrelat2i  32168  disjex  32375  disjexc  32376  meran1  35885  meran3  35887  bj-dfbi5  36040  bj-andnotim  36055  itg2addnclem2  37134  dvasin  37166  impor  37543  biimpor  37546  moeu2  37823  hlrelat2  38865  sticksstones1  41602  flt4lem7  42055  nna4b4nsq  42056  ifpim1  42871  ifpim2  42874  ifpidg  42893  ifpim23g  42897  ifpim123g  42902  ifpimimb  42906  ifpororb  42907  sqrtcvallem1  43033  hbimpgVD  44315  stoweidlem14  45374  fvmptrabdm  46645  fullthinc  48024  alimp-surprise  48185  eximp-surprise  48189