Theorem imor 854

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  imori  855  imorri  856  pm4.62  857  pm4.78  935  pm4.52  987  dfifp4  1067  dfifp5  1068  dfifp7  1070  norasslem1  1536  rb-bijust  1751  rb-imdf  1752  rb-ax1  1754  nf2  1787  relsnb  5758  soxp  8079  modom  9161  dffin7-2  10320  algcvgblem  16546  divgcdodd  16680  noinfprefixmo  27665  chrelat2i  32436  disjex  32662  disjexc  32663  meran1  36593  meran3  36595  bj-dfbi5  36839  bj-andnotim  36853  itg2addnclem2  37993  dvasin  38025  impor  38402  biimpor  38405  moeu2  38691  hlrelat2  39849  sticksstones1  42585  flt4lem7  43092  nna4b4nsq  43093  ifpim1  43896  ifpim2  43899  ifpidg  43918  ifpim23g  43922  ifpim123g  43927  ifpimimb  43931  ifpororb  43932  sqrtcvallem1  44058  hbimpgVD  45330  stoweidlem14  46442  fvmptrabdm  47741  fullthinc  49925  alimp-surprise  50255  eximp-surprise  50259