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  7312  canthwdom  9484  cardprclem  9891  ominf4  10222  canthp1lem2  10564  pwfseqlem4  10573  pwxpndom2  10576  lbioo  13292  ubioo  13293  fzp1disj  13499  fzonel  13589  fzouzdisj  13611  hashbclem  14375  harmonic  15782  eirrlem  16129  ruclem13  16167  prmreclem6  16849  4sqlem17  16889  vdwlem12  16920  vdwnnlem3  16925  mreexmrid  17566  psgnunilem3  19425  efgredlemb  19675  efgredlem  19676  00lss  20892  alexsublem  23988  ptcmplem4  23999  nmoleub2lem3  25071  dvferm1lem  25944  dvferm2lem  25946  plyeq0lem  26171  logno1  26601  lgsval2lem  27274  pntpbnd2  27554  ubico  32855  bnj1523  35227  antnest  35883  pm2.65ni  45287  lbioc  45755  salgencntex  46583