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  5439  canth  7306  canthwdom  9472  cardprclem  9879  ominf4  10210  canthp1lem2  10551  pwfseqlem4  10560  pwxpndom2  10563  lbioo  13278  ubioo  13279  fzp1disj  13485  fzonel  13575  fzouzdisj  13597  hashbclem  14361  harmonic  15768  eirrlem  16115  ruclem13  16153  prmreclem6  16835  4sqlem17  16875  vdwlem12  16906  vdwnnlem3  16911  mreexmrid  17551  psgnunilem3  19410  efgredlemb  19660  efgredlem  19661  00lss  20876  alexsublem  23960  ptcmplem4  23971  nmoleub2lem3  25043  dvferm1lem  25916  dvferm2lem  25918  plyeq0lem  26143  logno1  26573  lgsval2lem  27246  pntpbnd2  27526  ubico  32762  bnj1523  35104  antnest  35754  pm2.65ni  45167  lbioc  45637  salgencntex  46465