Theorem imor 428

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 304	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 339	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 385	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 267	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  imori  429  imorri  430  pm4.62  435  pm4.52  512  pm4.78  606  dfifp4  1016  dfifp5  1017  dfifp7  1019  rb-bijust  1674  rb-imdf  1675  rb-ax1  1677  nf2  1711  r19.30  3082  soxp  7290  modom  8161  dffin7-2  9220  algcvgblem  15290  divgcdodd  15422  chrelat2i  29224  disjex  29405  disjexc  29406  meran1  32410  meran3  32412  bj-dfbi5  32559  bj-andnotim  32573  itg2addnclem2  33462  dvasin  33496  impor  33880  biimpor  33883  hlrelat2  34689  ifpim1  37813  ifpim2  37816  ifpidg  37836  ifpim23g  37840  ifpim123g  37845  ifpimimb  37849  ifpororb  37850  hbimpgVD  39140  stoweidlem14  40231  alimp-surprise  42526  eximp-surprise  42530