Theorem imor 852

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  imori  853  imorri  854  pm4.62  855  pm4.78  934  pm4.52  984  dfifp4  1066  dfifp5  1067  dfifp7  1069  norasslem1  1536  rb-bijust  1752  rb-imdf  1753  rb-ax1  1755  nf2  1788  relsnb  5800  soxp  8110  modom  9240  dffin7-2  10389  algcvgblem  16510  divgcdodd  16643  noinfprefixmo  27184  chrelat2i  31596  disjex  31801  disjexc  31802  meran1  35234  meran3  35236  bj-dfbi5  35389  bj-andnotim  35404  itg2addnclem2  36478  dvasin  36510  impor  36887  biimpor  36890  moeu2  37169  hlrelat2  38212  sticksstones1  40900  flt4lem7  41345  nna4b4nsq  41346  ifpim1  42153  ifpim2  42156  ifpidg  42175  ifpim23g  42179  ifpim123g  42184  ifpimimb  42188  ifpororb  42189  sqrtcvallem1  42315  hbimpgVD  43598  stoweidlem14  44665  fvmptrabdm  45936  fullthinc  47568  alimp-surprise  47729  eximp-surprise  47733