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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.21dd  198  mto  200  mt2  203  0nelop  5470  canth  7354  pwuninel  8259  canthwdom  9529  cardprclem  9953  ominf4  10284  canthp1lem2  10626  pwfseqlem4  10635  pwxpndom2  10638  lbioo  13394  ubioo  13395  fzp1disj  13602  fzonel  13693  fzouzdisj  13715  hashbclem  14479  harmonic  15903  eirrlem  16250  ruclem13  16288  prmreclem6  16971  4sqlem17  17011  vdwlem12  17042  vdwnnlem3  17047  mreexmrid  17689  psgnunilem3  19557  efgredlemb  19807  efgredlem  19808  00lss  21031  alexsublem  24162  ptcmplem4  24173  nmoleub2lem3  25235  dvferm1lem  26104  dvferm2lem  26106  plyeq0lem  26328  logno1  26759  lgsval2lem  27429  pntpbnd2  27709  ubico  33032  bnj1523  35376  antnest  36052  elttcirr  36904  pm2.65ni  45624  lbioc  46087  salgencntex  46915