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  5410  canth  7229  sdom0OLD  8896  canthwdom  9338  cardprclem  9737  ominf4  10068  canthp1lem2  10409  pwfseqlem4  10418  pwxpndom2  10421  lbioo  13110  ubioo  13111  fzp1disj  13315  fzonel  13401  fzouzdisj  13423  hashbclem  14164  harmonic  15571  eirrlem  15913  ruclem13  15951  prmreclem6  16622  4sqlem17  16662  vdwlem12  16693  vdwnnlem3  16698  mreexmrid  17352  psgnunilem3  19104  efgredlemb  19352  efgredlem  19353  00lss  20203  alexsublem  23195  ptcmplem4  23206  nmoleub2lem3  24278  dvferm1lem  25148  dvferm2lem  25150  plyeq0lem  25371  logno1  25791  lgsval2lem  26455  pntpbnd2  26735  ubico  31096  bnj1523  33051  sn-inelr  40435  pm2.65ni  42592  lbioc  43051  salgencntex  43882