Theorem pm2.65i 184

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 133	. 2 ⊢ (𝜓 → ¬ 𝜑)
3		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	3	con3i 149	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
5	2, 4	pm2.61i 175	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  185  mto  187  mt2  190  noel  3878  0nelop  4886  canth  6508  sdom0  7977  canthwdom  8367  cardprclem  8688  ominf4  9017  canthp1lem2  9354  pwfseqlem4  9363  pwxpndom2  9366  lbioo  12077  ubioo  12078  fzp1disj  12269  fzonel  12352  fzouzdisj  12373  hashbclem  13093  harmonic  14430  eirrlem  14771  ruclem13  14810  prmreclem6  15463  4sqlem17  15503  vdwlem12  15534  vdwnnlem3  15539  mreexmrid  16126  psgnunilem3  17739  efgredlemb  17982  efgredlem  17983  00lss  18763  alexsublem  21658  ptcmplem4  21669  nmoleub2lem3  22723  dvferm1lem  23551  dvferm2lem  23553  plyeq0lem  23770  logno1  24182  lgsval2lem  24832  pntpbnd2  25076  ubico  28927  bnj1523  30393  pm2.65ni  38235  lbioc  38586  salgencntex  39237