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  5484  canth  7377  pwuninel  8280  canthwdom  9551  cardprclem  9984  ominf4  10314  canthp1lem2  10656  pwfseqlem4  10665  pwxpndom2  10668  lbioo  13421  ubioo  13422  fzp1disj  13630  fzonel  13721  fzouzdisj  13743  hashbclem  14509  harmonic  15939  eirrlem  16285  ruclem13  16323  prmreclem6  17006  4sqlem17  17046  vdwlem12  17077  vdwnnlem3  17082  mreexmrid  17724  psgnunilem3  19597  efgredlemb  19847  efgredlem  19848  00lss  21099  alexsublem  24238  ptcmplem4  24249  nmoleub2lem3  25311  dvferm1lem  26180  dvferm2lem  26182  plyeq0lem  26404  logno1  26838  lgsval2lem  27508  pntpbnd2  27788  ubico  33157  bnj1523  35491  antnest  36202  elttcirr  37083  pm2.65ni  45807  lbioc  46270  salgencntex  47098