Theorem imor 849

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 314	. . 3 ⊢ (𝜑 ↔ ¬ ¬ 𝜑)
2	1	imbi1i 349	. 2 ⊢ ((𝜑 → 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
3		df-or 844	. 2 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (¬ ¬ 𝜑 → 𝜓))
4	2, 3	bitr4i 277	1 ⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))

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

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 844

This theorem is referenced by:  imori  850  imorri  851  pm4.62  852  pm4.78  931  pm4.52  981  dfifp4  1063  dfifp5  1064  dfifp7  1066  norasslem1  1532  rb-bijust  1753  rb-imdf  1754  rb-ax1  1756  nf2  1789  relsnb  5701  soxp  7941  modom  8953  dffin7-2  10085  algcvgblem  16210  divgcdodd  16343  chrelat2i  30628  disjex  30832  disjexc  30833  noinfprefixmo  33831  meran1  34527  meran3  34529  bj-dfbi5  34682  bj-andnotim  34697  itg2addnclem2  35756  dvasin  35788  impor  36166  biimpor  36169  hlrelat2  37344  sticksstones1  40030  flt4lem7  40412  nna4b4nsq  40413  ifpim1  40974  ifpim2  40977  ifpidg  40996  ifpim23g  41000  ifpim123g  41005  ifpimimb  41009  ifpororb  41010  sqrtcvallem1  41128  hbimpgVD  42413  stoweidlem14  43445  fvmptrabdm  44672  fullthinc  46215  alimp-surprise  46370  eximp-surprise  46374