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  5746  soxp  8065  modom  9142  dffin7-2  10296  algcvgblem  16490  divgcdodd  16623  noinfprefixmo  27641  chrelat2i  32347  disjex  32574  disjexc  32575  meran1  36476  meran3  36478  bj-dfbi5  36639  bj-andnotim  36653  itg2addnclem2  37732  dvasin  37764  impor  38141  biimpor  38144  moeu2  38414  hlrelat2  39522  sticksstones1  42259  flt4lem7  42777  nna4b4nsq  42778  ifpim1  43586  ifpim2  43589  ifpidg  43608  ifpim23g  43612  ifpim123g  43617  ifpimimb  43621  ifpororb  43622  sqrtcvallem1  43748  hbimpgVD  45020  stoweidlem14  46136  fvmptrabdm  47417  fullthinc  49575  alimp-surprise  49905  eximp-surprise  49909