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  4296  0nelop  5385  canth  7110  sdom0  8648  canthwdom  9042  cardprclem  9407  ominf4  9733  canthp1lem2  10074  pwfseqlem4  10083  pwxpndom2  10086  lbioo  12768  ubioo  12769  fzp1disj  12965  fzonel  13050  fzouzdisj  13072  hashbclem  13809  harmonic  15213  eirrlem  15556  ruclem13  15594  prmreclem6  16256  4sqlem17  16296  vdwlem12  16327  vdwnnlem3  16332  mreexmrid  16913  psgnunilem3  18623  efgredlemb  18871  efgredlem  18872  00lss  19712  alexsublem  22651  ptcmplem4  22662  nmoleub2lem3  23718  dvferm1lem  24580  dvferm2lem  24582  plyeq0lem  24799  logno1  25218  lgsval2lem  25882  pntpbnd2  26162  ubico  30497  bnj1523  32343  pm2.65ni  41304  lbioc  41787  salgencntex  42625