Theorem pm2.65i 195

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 183	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  196  mto  198  mt2  201  0nelop  5444  canth  7317  canthwdom  9491  cardprclem  9901  ominf4  10232  canthp1lem2  10574  pwfseqlem4  10583  pwxpndom2  10586  lbioo  13327  ubioo  13328  fzp1disj  13535  fzonel  13626  fzouzdisj  13648  hashbclem  14412  harmonic  15822  eirrlem  16169  ruclem13  16207  prmreclem6  16890  4sqlem17  16930  vdwlem12  16961  vdwnnlem3  16966  mreexmrid  17607  psgnunilem3  19469  efgredlemb  19719  efgredlem  19720  00lss  20938  alexsublem  24034  ptcmplem4  24045  nmoleub2lem3  25107  dvferm1lem  25976  dvferm2lem  25978  plyeq0lem  26200  logno1  26625  lgsval2lem  27295  pntpbnd2  27575  ubico  32874  bnj1523  35260  antnest  35924  elttcirr  36766  pm2.65ni  45501  lbioc  45965  salgencntex  46793