Theorem pm2.65i 195

Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) (Proof shortened by Garrett Katz, 7-Jun-2026.)

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		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl3 138	. 2 ⊢ (𝜑 → ¬ 𝜑)
4	3	pm2.01i 190	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  0nelop  5464  canth  7346  pwuninel  8250  canthwdom  9524  cardprclem  9934  ominf4  10266  canthp1lem2  10608  pwfseqlem4  10617  pwxpndom2  10620  lbioo  13377  ubioo  13378  fzp1disj  13585  fzonel  13676  fzouzdisj  13698  hashbclem  14462  harmonic  15872  eirrlem  16219  ruclem13  16257  prmreclem6  16940  4sqlem17  16980  vdwlem12  17011  vdwnnlem3  17016  mreexmrid  17658  psgnunilem3  19519  efgredlemb  19769  efgredlem  19770  00lss  20988  alexsublem  24084  ptcmplem4  24095  nmoleub2lem3  25157  dvferm1lem  26026  dvferm2lem  26028  plyeq0lem  26250  logno1  26678  lgsval2lem  27348  pntpbnd2  27628  ubico  32927  bnj1523  35330  antnest  36003  elttcirr  36855  pm2.65ni  45590  lbioc  46053  salgencntex  46881