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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ 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 210  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  1535  rb-bijust  1756  rb-imdf  1757  rb-ax1  1759  nf2  1792  relsnb  5640  soxp  7842  modom  8791  dffin7-2  9891  algcvgblem  16011  divgcdodd  16144  chrelat2i  30292  disjex  30497  disjexc  30498  noinfprefixmo  33537  meran1  34230  meran3  34232  bj-dfbi5  34382  bj-andnotim  34397  itg2addnclem2  35441  dvasin  35473  impor  35851  biimpor  35854  hlrelat2  37029  sticksstones1  39697  flt4lem7  40052  nna4b4nsq  40053  ifpim1  40614  ifpim2  40617  ifpidg  40636  ifpim23g  40640  ifpim123g  40645  ifpimimb  40649  ifpororb  40650  sqrtcvallem1  40768  hbimpgVD  42046  stoweidlem14  43081  fvmptrabdm  44302  alimp-surprise  45921  eximp-surprise  45925