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  5467  canth  7374  pwuninel  8295  canthwdom  9576  cardprclem  10063  ominf4  10393  canthp1lem2  10741  pwfseqlem4  10750  pwxpndom2  10753  lbioo  13510  ubioo  13511  fzp1disj  13720  fzonel  13811  fzouzdisj  13833  hashbclem  14600  harmonic  16033  eirrlem  16377  ruclem13  16415  prmreclem6  17104  4sqlem17  17144  vdwlem12  17175  vdwnnlem3  17180  mreexmrid  17822  psgnunilem3  19715  efgredlemb  19965  efgredlem  19966  00lss  21221  alexsublem  24368  ptcmplem4  24379  nmoleub2lem3  25441  dvferm1lem  26309  dvferm2lem  26311  plyeq0lem  26534  logno1  26969  lgsval2lem  27639  pntpbnd2  27919  ubico  33413  bnj1523  35747  antnest  36540  mirimanoffr  36546  elttcirr  37411  pm2.65ni  46156  lbioc  46618  salgencntex  47446