Theorem imor 853

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 847

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 848

This theorem is referenced by:  imori  854  imorri  855  pm4.62  856  pm4.78  934  pm4.52  986  dfifp4  1066  dfifp5  1067  dfifp7  1069  norasslem1  1535  rb-bijust  1750  rb-imdf  1751  rb-ax1  1753  nf2  1786  relsnb  5742  soxp  8059  modom  9135  dffin7-2  10286  algcvgblem  16485  divgcdodd  16618  noinfprefixmo  27638  chrelat2i  32340  disjex  32567  disjexc  32568  meran1  36444  meran3  36446  bj-dfbi5  36607  bj-andnotim  36621  itg2addnclem2  37711  dvasin  37743  impor  38120  biimpor  38123  moeu2  38389  hlrelat2  39441  sticksstones1  42178  flt4lem7  42691  nna4b4nsq  42692  ifpim1  43501  ifpim2  43504  ifpidg  43523  ifpim23g  43527  ifpim123g  43532  ifpimimb  43536  ifpororb  43537  sqrtcvallem1  43663  hbimpgVD  44935  stoweidlem14  46051  fvmptrabdm  47323  fullthinc  49481  alimp-surprise  49811  eximp-surprise  49815