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  5759  soxp  8081  modom  9163  dffin7-2  10320  algcvgblem  16516  divgcdodd  16649  noinfprefixmo  27681  chrelat2i  32452  disjex  32678  disjexc  32679  meran1  36624  meran3  36626  bj-dfbi5  36795  bj-andnotim  36809  itg2addnclem2  37917  dvasin  37949  impor  38326  biimpor  38329  moeu2  38615  hlrelat2  39773  sticksstones1  42510  flt4lem7  43011  nna4b4nsq  43012  ifpim1  43819  ifpim2  43822  ifpidg  43841  ifpim23g  43845  ifpim123g  43850  ifpimimb  43854  ifpororb  43855  sqrtcvallem1  43981  hbimpgVD  45253  stoweidlem14  46366  fvmptrabdm  47647  fullthinc  49803  alimp-surprise  50133  eximp-surprise  50137