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  5450  canth  7321  canthwdom  9494  cardprclem  9903  ominf4  10234  canthp1lem2  10576  pwfseqlem4  10585  pwxpndom2  10588  lbioo  13329  ubioo  13330  fzp1disj  13537  fzonel  13628  fzouzdisj  13650  hashbclem  14414  harmonic  15824  eirrlem  16171  ruclem13  16209  prmreclem6  16892  4sqlem17  16932  vdwlem12  16963  vdwnnlem3  16968  mreexmrid  17609  psgnunilem3  19471  efgredlemb  19721  efgredlem  19722  00lss  20936  alexsublem  24009  ptcmplem4  24020  nmoleub2lem3  25082  dvferm1lem  25951  dvferm2lem  25953  plyeq0lem  26175  logno1  26600  lgsval2lem  27270  pntpbnd2  27550  ubico  32848  bnj1523  35213  antnest  35871  elttcirr  36713  pm2.65ni  45477  lbioc  45943  salgencntex  46771