Theorem imor 853

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

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

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 848

This theorem is referenced by:  imori  854  imorri  855  pm4.62  856  pm4.78  934  pm4.52  986  dfifp4  1066  dfifp5  1067  dfifp7  1069  norasslem1  1534  rb-bijust  1749  rb-imdf  1750  rb-ax1  1752  nf2  1785  relsnb  5749  soxp  8069  modom  9150  dffin7-2  10311  algcvgblem  16506  divgcdodd  16639  noinfprefixmo  27629  chrelat2i  32327  disjex  32554  disjexc  32555  meran1  36384  meran3  36386  bj-dfbi5  36547  bj-andnotim  36561  itg2addnclem2  37651  dvasin  37683  impor  38060  biimpor  38063  moeu2  38329  hlrelat2  39382  sticksstones1  42119  flt4lem7  42632  nna4b4nsq  42633  ifpim1  43442  ifpim2  43445  ifpidg  43464  ifpim23g  43468  ifpim123g  43473  ifpimimb  43477  ifpororb  43478  sqrtcvallem1  43604  hbimpgVD  44877  stoweidlem14  45996  fvmptrabdm  47278  fullthinc  49436  alimp-surprise  49766  eximp-surprise  49770