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  5501  canth  7385  sdom0OLD  9149  canthwdom  9619  cardprclem  10019  ominf4  10352  canthp1lem2  10693  pwfseqlem4  10702  pwxpndom2  10705  lbioo  13418  ubioo  13419  fzp1disj  13623  fzonel  13713  fzouzdisj  13735  hashbclem  14491  harmonic  15895  eirrlem  16240  ruclem13  16278  prmreclem6  16959  4sqlem17  16999  vdwlem12  17030  vdwnnlem3  17035  mreexmrid  17686  psgnunilem3  19514  efgredlemb  19764  efgredlem  19765  00lss  20939  alexsublem  24052  ptcmplem4  24063  nmoleub2lem3  25148  dvferm1lem  26022  dvferm2lem  26024  plyeq0lem  26249  logno1  26678  lgsval2lem  27351  pntpbnd2  27631  ubico  32777  bnj1523  35085  antnest  35694  sn-inelr  42497  pm2.65ni  45051  lbioc  45526  salgencntex  46358