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 206   ∨ 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 207  df-or 847

This theorem is referenced by:  imori  853  imorri  854  pm4.62  855  pm4.78  933  pm4.52  985  dfifp4  1067  dfifp5  1068  dfifp7  1070  norasslem1  1531  rb-bijust  1747  rb-imdf  1748  rb-ax1  1750  nf2  1783  relsnb  5826  soxp  8170  modom  9307  dffin7-2  10467  algcvgblem  16624  divgcdodd  16757  noinfprefixmo  27764  chrelat2i  32397  disjex  32614  disjexc  32615  meran1  36377  meran3  36379  bj-dfbi5  36540  bj-andnotim  36554  itg2addnclem2  37632  dvasin  37664  impor  38041  biimpor  38044  moeu2  38318  hlrelat2  39360  sticksstones1  42103  flt4lem7  42614  nna4b4nsq  42615  ifpim1  43431  ifpim2  43434  ifpidg  43453  ifpim23g  43457  ifpim123g  43462  ifpimimb  43466  ifpororb  43467  sqrtcvallem1  43593  hbimpgVD  44875  stoweidlem14  45935  fvmptrabdm  47208  fullthinc  48713  alimp-surprise  48874  eximp-surprise  48878