Theorem imor 854

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

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

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 849

This theorem is referenced by:  imori  855  imorri  856  pm4.62  857  pm4.78  935  pm4.52  987  dfifp4  1067  dfifp5  1068  dfifp7  1070  norasslem1  1534  rb-bijust  1749  rb-imdf  1750  rb-ax1  1752  nf2  1785  relsnb  5812  soxp  8154  modom  9280  dffin7-2  10438  algcvgblem  16614  divgcdodd  16747  noinfprefixmo  27746  chrelat2i  32384  disjex  32605  disjexc  32606  meran1  36412  meran3  36414  bj-dfbi5  36575  bj-andnotim  36589  itg2addnclem2  37679  dvasin  37711  impor  38088  biimpor  38091  moeu2  38363  hlrelat2  39405  sticksstones1  42147  flt4lem7  42669  nna4b4nsq  42670  ifpim1  43482  ifpim2  43485  ifpidg  43504  ifpim23g  43508  ifpim123g  43513  ifpimimb  43517  ifpororb  43518  sqrtcvallem1  43644  hbimpgVD  44924  stoweidlem14  46029  fvmptrabdm  47305  fullthinc  49099  alimp-surprise  49299  eximp-surprise  49303