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 ⊢ ¬ 𝜑

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.21dd  198  mto  200  mt2  203  0nelop  5477  canth  7371  pwuninel  8277  canthwdom  9555  cardprclem  9988  ominf4  10318  canthp1lem2  10666  pwfseqlem4  10675  pwxpndom2  10678  lbioo  13433  ubioo  13434  fzp1disj  13642  fzonel  13733  fzouzdisj  13755  hashbclem  14521  harmonic  15952  eirrlem  16298  ruclem13  16336  prmreclem6  17019  4sqlem17  17059  vdwlem12  17090  vdwnnlem3  17095  mreexmrid  17737  psgnunilem3  19629  efgredlemb  19879  efgredlem  19880  00lss  21131  alexsublem  24276  ptcmplem4  24287  nmoleub2lem3  25349  dvferm1lem  26218  dvferm2lem  26220  plyeq0lem  26443  logno1  26881  lgsval2lem  27551  pntpbnd2  27831  ubico  33254  bnj1523  35588  antnest  36276  elttcirr  37158  pm2.65ni  45888  lbioc  46351  salgencntex  47179