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  5452  canth  7322  canthwdom  9496  cardprclem  9903  ominf4  10234  canthp1lem2  10576  pwfseqlem4  10585  pwxpndom2  10588  lbioo  13304  ubioo  13305  fzp1disj  13511  fzonel  13601  fzouzdisj  13623  hashbclem  14387  harmonic  15794  eirrlem  16141  ruclem13  16179  prmreclem6  16861  4sqlem17  16901  vdwlem12  16932  vdwnnlem3  16937  mreexmrid  17578  psgnunilem3  19437  efgredlemb  19687  efgredlem  19688  00lss  20904  alexsublem  24000  ptcmplem4  24011  nmoleub2lem3  25083  dvferm1lem  25956  dvferm2lem  25958  plyeq0lem  26183  logno1  26613  lgsval2lem  27286  pntpbnd2  27566  ubico  32865  bnj1523  35246  antnest  35902  pm2.65ni  45400  lbioc  45867  salgencntex  46695