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  5440  canth  7290  sdom0OLD  8974  canthwdom  9436  cardprclem  9836  ominf4  10169  canthp1lem2  10510  pwfseqlem4  10519  pwxpndom2  10522  lbioo  13211  ubioo  13212  fzp1disj  13416  fzonel  13502  fzouzdisj  13524  hashbclem  14264  harmonic  15670  eirrlem  16012  ruclem13  16050  prmreclem6  16719  4sqlem17  16759  vdwlem12  16790  vdwnnlem3  16795  mreexmrid  17449  psgnunilem3  19200  efgredlemb  19447  efgredlem  19448  00lss  20309  alexsublem  23301  ptcmplem4  23312  nmoleub2lem3  24384  dvferm1lem  25254  dvferm2lem  25256  plyeq0lem  25477  logno1  25897  lgsval2lem  26561  pntpbnd2  26841  ubico  31383  bnj1523  33350  sn-inelr  40695  pm2.65ni  42912  lbioc  43387  salgencntex  44218