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  5443  canth  7307  canthwdom  9490  cardprclem  9894  ominf4  10225  canthp1lem2  10566  pwfseqlem4  10575  pwxpndom2  10578  lbioo  13297  ubioo  13298  fzp1disj  13504  fzonel  13594  fzouzdisj  13616  hashbclem  14377  harmonic  15784  eirrlem  16131  ruclem13  16169  prmreclem6  16851  4sqlem17  16891  vdwlem12  16922  vdwnnlem3  16927  mreexmrid  17567  psgnunilem3  19393  efgredlemb  19643  efgredlem  19644  00lss  20862  alexsublem  23947  ptcmplem4  23958  nmoleub2lem3  25031  dvferm1lem  25904  dvferm2lem  25906  plyeq0lem  26131  logno1  26561  lgsval2lem  27234  pntpbnd2  27514  ubico  32731  bnj1523  35037  antnest  35661  pm2.65ni  45024  lbioc  45495  salgencntex  46325