Theorem pm2.65i 196

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 141	. 2 ⊢ (𝜓 → ¬ 𝜑)
3		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	3	con3i 157	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
5	2, 4	pm2.61i 184	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  197  mto  199  mt2  202  noelOLD  4297  0nelop  5386  canth  7111  sdom0  8649  canthwdom  9043  cardprclem  9408  ominf4  9734  canthp1lem2  10075  pwfseqlem4  10084  pwxpndom2  10087  lbioo  12770  ubioo  12771  fzp1disj  12967  fzonel  13052  fzouzdisj  13074  hashbclem  13811  harmonic  15214  eirrlem  15557  ruclem13  15595  prmreclem6  16257  4sqlem17  16297  vdwlem12  16328  vdwnnlem3  16333  mreexmrid  16914  psgnunilem3  18624  efgredlemb  18872  efgredlem  18873  00lss  19713  alexsublem  22652  ptcmplem4  22663  nmoleub2lem3  23719  dvferm1lem  24581  dvferm2lem  24583  plyeq0lem  24800  logno1  25219  lgsval2lem  25883  pntpbnd2  26163  ubico  30498  bnj1523  32343  pm2.65ni  41326  lbioc  41809  salgencntex  42646