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  5473  canth  7400  pwuninel  8323  canthwdom  9603  cardprclem  10090  ominf4  10420  canthp1lem2  10768  pwfseqlem4  10777  pwxpndom2  10780  lbioo  13537  ubioo  13538  fzp1disj  13747  fzonel  13838  fzouzdisj  13860  hashbclem  14627  harmonic  16060  eirrlem  16404  ruclem13  16442  prmreclem6  17131  4sqlem17  17171  vdwlem12  17202  vdwnnlem3  17207  mreexmrid  17849  psgnunilem3  19743  efgredlemb  19993  efgredlem  19994  00lss  21249  alexsublem  24396  ptcmplem4  24407  nmoleub2lem3  25469  dvferm1lem  26337  dvferm2lem  26339  plyeq0lem  26562  logno1  26997  lgsval2lem  27667  pntpbnd2  27947  ubico  33440  bnj1523  35784  antnest  36634  mirimanoffr  36640  elttcirr  37510  pm2.65ni  46279  lbioc  46740  salgencntex  47568