Theorem pm2.65i 183

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 132	. 2 ⊢ (𝜓 → ¬ 𝜑)
3		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	3	con3i 148	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
5	2, 4	pm2.61i 174	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  184  mto  186  mt2  189  noel  3877  0nelop  4880  canth  6486  sdom0  7954  canthwdom  8344  cardprclem  8665  ominf4  8994  canthp1lem2  9331  pwfseqlem4  9340  pwxpndom2  9343  lbioo  12033  ubioo  12034  fzp1disj  12224  fzonel  12307  fzouzdisj  12328  hashbclem  13045  harmonic  14376  eirrlem  14717  ruclem13  14756  prmreclem6  15409  4sqlem17  15449  vdwlem12  15480  vdwnnlem3  15485  mreexmrid  16072  psgnunilem3  17685  efgredlemb  17928  efgredlem  17929  00lss  18709  alexsublem  21600  ptcmplem4  21611  nmoleub2lem3  22654  dvferm1lem  23468  dvferm2lem  23470  plyeq0lem  23687  logno1  24099  lgsval2lem  24749  pntpbnd2  24993  ubico  28733  bnj1523  30199  pm2.65ni  38031  lbioc  38383  salgencntex  39034