Theorem pm2.65i 194

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  195  mto  197  mt2  200  0nelop  5506  canth  7385  sdom0OLD  9148  canthwdom  9617  cardprclem  10017  ominf4  10350  canthp1lem2  10691  pwfseqlem4  10700  pwxpndom2  10703  lbioo  13415  ubioo  13416  fzp1disj  13620  fzonel  13710  fzouzdisj  13732  hashbclem  14488  harmonic  15892  eirrlem  16237  ruclem13  16275  prmreclem6  16955  4sqlem17  16995  vdwlem12  17026  vdwnnlem3  17031  mreexmrid  17688  psgnunilem3  19529  efgredlemb  19779  efgredlem  19780  00lss  20957  alexsublem  24068  ptcmplem4  24079  nmoleub2lem3  25162  dvferm1lem  26037  dvferm2lem  26039  plyeq0lem  26264  logno1  26693  lgsval2lem  27366  pntpbnd2  27646  ubico  32784  bnj1523  35064  antnest  35674  sn-inelr  42474  pm2.65ni  44984  lbioc  45466  salgencntex  46299