Theorem imor 427

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 303	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 338	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 384	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 266	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  imori  428  imorri  429  pm4.62  434  pm4.52  511  pm4.78  604  dfifp4  1010  dfifp5  1011  dfifp7  1013  rb-bijust  1665  rb-imdf  1666  rb-ax1  1668  nf2  1702  r19.30  3063  soxp  7177  modom  8046  dffin7-2  9103  algcvgblem  15128  divgcdodd  15260  chrelat2i  28608  disjex  28787  disjexc  28788  meran1  31580  meran3  31582  bj-dfbi5  31729  bj-andnotim  31746  bj-nf2  31766  itg2addnclem2  32632  dvasin  32666  impor  33050  biimpor  33053  hlrelat2  33707  ifpim1  36832  ifpim2  36835  ifpidg  36855  ifpim23g  36859  ifpim123g  36864  ifpimimb  36868  ifpororb  36869  hbimpgVD  38162  stoweidlem14  38907  alimp-surprise  42335  eximp-surprise  42339