Theorem pm2.65i 196

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 139	. 2 ⊢ (𝜑 → ¬ 𝜑)
4	3	pm2.01i 191	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  198  mto  200  mt2  203  0nelop  5481  canth  7366  pwuninel  8272  canthwdom  9542  cardprclem  9966  ominf4  10297  canthp1lem2  10639  pwfseqlem4  10648  pwxpndom2  10651  lbioo  13404  ubioo  13405  fzp1disj  13613  fzonel  13704  fzouzdisj  13726  hashbclem  14491  harmonic  15915  eirrlem  16261  ruclem13  16299  prmreclem6  16982  4sqlem17  17022  vdwlem12  17053  vdwnnlem3  17058  mreexmrid  17700  psgnunilem3  19567  efgredlemb  19817  efgredlem  19818  00lss  21043  alexsublem  24182  ptcmplem4  24193  nmoleub2lem3  25255  dvferm1lem  26124  dvferm2lem  26126  plyeq0lem  26348  logno1  26782  lgsval2lem  27452  pntpbnd2  27732  ubico  33101  bnj1523  35440  antnest  36162  elttcirr  37023  pm2.65ni  45749  lbioc  46212  salgencntex  47040