Theorem pm2.65i 185

Description: Inference rule 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 134	. 2 ⊢ (𝜓 → ¬ 𝜑)
3		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	3	con3i 150	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
5	2, 4	pm2.61i 176	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  186  mto  188  mt2  191  noel  3952  0nelop  4989  canth  6648  sdom0  8133  canthwdom  8525  cardprclem  8843  ominf4  9172  canthp1lem2  9513  pwfseqlem4  9522  pwxpndom2  9525  lbioo  12244  ubioo  12245  fzp1disj  12437  fzonel  12522  fzouzdisj  12543  hashbclem  13274  harmonic  14635  eirrlem  14976  ruclem13  15015  prmreclem6  15672  4sqlem17  15712  vdwlem12  15743  vdwnnlem3  15748  mreexmrid  16350  psgnunilem3  17962  efgredlemb  18205  efgredlem  18206  00lss  18990  alexsublem  21895  ptcmplem4  21906  nmoleub2lem3  22961  dvferm1lem  23792  dvferm2lem  23794  plyeq0lem  24011  logno1  24427  lgsval2lem  25077  pntpbnd2  25321  ubico  29665  bnj1523  31265  pm2.65ni  39524  lbioc  40057  salgencntex  40879