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  5468  canth  7366  pwuninel  8276  canthwdom  9557  cardprclem  10041  ominf4  10371  canthp1lem2  10719  pwfseqlem4  10728  pwxpndom2  10731  lbioo  13488  ubioo  13489  fzp1disj  13697  fzonel  13788  fzouzdisj  13810  hashbclem  14577  harmonic  16008  eirrlem  16352  ruclem13  16390  prmreclem6  17079  4sqlem17  17119  vdwlem12  17150  vdwnnlem3  17155  mreexmrid  17797  psgnunilem3  19690  efgredlemb  19940  efgredlem  19941  00lss  21196  alexsublem  24343  ptcmplem4  24354  nmoleub2lem3  25416  dvferm1lem  26284  dvferm2lem  26286  plyeq0lem  26509  logno1  26946  lgsval2lem  27616  pntpbnd2  27896  ubico  33349  bnj1523  35684  antnest  36423  elttcirr  37289  pm2.65ni  46006  lbioc  46469  salgencntex  47297