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  5471  canth  7359  sdom0OLD  9123  canthwdom  9593  cardprclem  9993  ominf4  10326  canthp1lem2  10667  pwfseqlem4  10676  pwxpndom2  10679  lbioo  13393  ubioo  13394  fzp1disj  13600  fzonel  13690  fzouzdisj  13712  hashbclem  14470  harmonic  15875  eirrlem  16222  ruclem13  16260  prmreclem6  16941  4sqlem17  16981  vdwlem12  17012  vdwnnlem3  17017  mreexmrid  17655  psgnunilem3  19477  efgredlemb  19727  efgredlem  19728  00lss  20898  alexsublem  23982  ptcmplem4  23993  nmoleub2lem3  25066  dvferm1lem  25940  dvferm2lem  25942  plyeq0lem  26167  logno1  26597  lgsval2lem  27270  pntpbnd2  27550  ubico  32752  bnj1523  35102  antnest  35711  sn-inelr  42510  pm2.65ni  45070  lbioc  45542  salgencntex  46372