Theorem pm2.65i 186

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 137	. 2 ⊢ (𝜓 → ¬ 𝜑)
3		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	3	con3i 152	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
5	2, 4	pm2.61i 177	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  187  mto  189  mt2  192  noelOLD  4147  0nelop  5193  canth  6882  sdom0  8382  canthwdom  8775  cardprclem  9140  ominf4  9471  canthp1lem2  9812  pwfseqlem4  9821  pwxpndom2  9824  lbioo  12522  ubioo  12523  fzp1disj  12721  fzonel  12806  fzouzdisj  12827  hashbclem  13554  harmonic  14999  eirrlem  15340  ruclem13  15379  prmreclem6  16033  4sqlem17  16073  vdwlem12  16104  vdwnnlem3  16109  mreexmrid  16693  psgnunilem3  18304  efgredlemb  18548  efgredlem  18549  efgredlemOLD  18550  00lss  19338  alexsublem  22260  ptcmplem4  22271  nmoleub2lem3  23326  dvferm1lem  24188  dvferm2lem  24190  plyeq0lem  24407  logno1  24823  lgsval2lem  25488  pntpbnd2  25732  ubico  30105  bnj1523  31742  pm2.65ni  40152  lbioc  40658  salgencntex  41495