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  5444  canth  7314  canthwdom  9487  cardprclem  9894  ominf4  10225  canthp1lem2  10567  pwfseqlem4  10576  pwxpndom2  10579  lbioo  13320  ubioo  13321  fzp1disj  13528  fzonel  13619  fzouzdisj  13641  hashbclem  14405  harmonic  15815  eirrlem  16162  ruclem13  16200  prmreclem6  16883  4sqlem17  16923  vdwlem12  16954  vdwnnlem3  16959  mreexmrid  17600  psgnunilem3  19462  efgredlemb  19712  efgredlem  19713  00lss  20927  alexsublem  24019  ptcmplem4  24030  nmoleub2lem3  25092  dvferm1lem  25961  dvferm2lem  25963  plyeq0lem  26185  logno1  26613  lgsval2lem  27284  pntpbnd2  27564  ubico  32863  bnj1523  35229  antnest  35887  elttcirr  36729  pm2.65ni  45495  lbioc  45961  salgencntex  46789