Theorem pm2.65i 193

Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
pm2.65i.1	⊢ (𝜑 → 𝜓)
pm2.65i.2	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.65i	⊢ ¬ 𝜑

Proof of Theorem pm2.65i

Step	Hyp	Ref	Expression
1		pm2.65i.2	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2	1	con2i 139	. 2 ⊢ (𝜓 → ¬ 𝜑)
3		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	3	con3i 154	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
5	2, 4	pm2.61i 182	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.21dd  194  mto  196  mt2  199  0nelop  5498  canth  7372  sdom0OLD  9134  canthwdom  9604  cardprclem  10004  ominf4  10337  canthp1lem2  10678  pwfseqlem4  10687  pwxpndom2  10690  lbioo  13390  ubioo  13391  fzp1disj  13595  fzonel  13681  fzouzdisj  13703  hashbclem  14447  harmonic  15841  eirrlem  16184  ruclem13  16222  prmreclem6  16893  4sqlem17  16933  vdwlem12  16964  vdwnnlem3  16969  mreexmrid  17626  psgnunilem3  19463  efgredlemb  19713  efgredlem  19714  00lss  20837  alexsublem  23992  ptcmplem4  24003  nmoleub2lem3  25086  dvferm1lem  25960  dvferm2lem  25962  plyeq0lem  26189  logno1  26615  lgsval2lem  27285  pntpbnd2  27565  ubico  32625  bnj1523  34833  sn-inelr  42155  pm2.65ni  44550  lbioc  45036  salgencntex  45869