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  5495  canth  7364  sdom0OLD  9111  canthwdom  9576  cardprclem  9976  ominf4  10309  canthp1lem2  10650  pwfseqlem4  10659  pwxpndom2  10662  lbioo  13359  ubioo  13360  fzp1disj  13564  fzonel  13650  fzouzdisj  13672  hashbclem  14415  harmonic  15809  eirrlem  16151  ruclem13  16189  prmreclem6  16858  4sqlem17  16898  vdwlem12  16929  vdwnnlem3  16934  mreexmrid  17591  psgnunilem3  19405  efgredlemb  19655  efgredlem  19656  00lss  20696  alexsublem  23768  ptcmplem4  23779  nmoleub2lem3  24862  dvferm1lem  25736  dvferm2lem  25738  plyeq0lem  25959  logno1  26380  lgsval2lem  27046  pntpbnd2  27326  ubico  32253  bnj1523  34380  sn-inelr  41640  pm2.65ni  44032  lbioc  44524  salgencntex  45357