Theorem imor 859

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 316	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 350	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 854	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 279	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  imori  860  imorri  861  pm4.62  862  pm4.78  940  pm4.52  992  dfifp4  1072  dfifp5  1073  dfifp7  1075  norasslem1  1541  rb-bijust  1756  rb-imdf  1757  rb-ax1  1759  nf2  1792  relsnb  5752  soxp  8076  modom  9158  dffin7-2  10318  algcvgblem  16544  divgcdodd  16678  noinfprefixmo  27690  chrelat2i  32461  disjex  32688  disjexc  32689  meran1  36646  meran3  36648  bj-dfbi5  36892  bj-andnotim  36906  itg2addnclem2  38046  dvasin  38078  impor  38455  biimpor  38458  moeu2  38744  hlrelat2  39902  sticksstones1  42638  flt4lem7  43116  nna4b4nsq  43117  ifpim1  43920  ifpim2  43923  ifpidg  43942  ifpim23g  43946  ifpim123g  43951  ifpimimb  43955  ifpororb  43956  sqrtcvallem1  44082  hbimpgVD  45354  stoweidlem14  46464  fvmptrabdm  47763  fullthinc  49947  alimp-surprise  50277  eximp-surprise  50281