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  1531  rb-bijust  1746  rb-imdf  1747  rb-ax1  1749  nf2  1782  relsnb  5815  soxp  8153  modom  9278  dffin7-2  10436  algcvgblem  16611  divgcdodd  16744  noinfprefixmo  27761  chrelat2i  32394  disjex  32612  disjexc  32613  meran1  36394  meran3  36396  bj-dfbi5  36557  bj-andnotim  36571  itg2addnclem2  37659  dvasin  37691  impor  38068  biimpor  38071  moeu2  38344  hlrelat2  39386  sticksstones1  42128  flt4lem7  42646  nna4b4nsq  42647  ifpim1  43459  ifpim2  43462  ifpidg  43481  ifpim23g  43485  ifpim123g  43490  ifpimimb  43494  ifpororb  43495  sqrtcvallem1  43621  hbimpgVD  44902  stoweidlem14  45970  fvmptrabdm  47243  fullthinc  48846  alimp-surprise  49011  eximp-surprise  49015