Theorem pm2.65i 193

Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

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	1	con2i 139	. 2 ⊢ (𝜓 → ¬ 𝜑)
3		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	3	con3i 154	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
5	2, 4	pm2.61i 182	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  194  mto  196  mt2  199  0nelop  5404  canth  7209  sdom0  8845  canthwdom  9268  cardprclem  9668  ominf4  9999  canthp1lem2  10340  pwfseqlem4  10349  pwxpndom2  10352  lbioo  13039  ubioo  13040  fzp1disj  13244  fzonel  13329  fzouzdisj  13351  hashbclem  14092  harmonic  15499  eirrlem  15841  ruclem13  15879  prmreclem6  16550  4sqlem17  16590  vdwlem12  16621  vdwnnlem3  16626  mreexmrid  17269  psgnunilem3  19019  efgredlemb  19267  efgredlem  19268  00lss  20118  alexsublem  23103  ptcmplem4  23114  nmoleub2lem3  24184  dvferm1lem  25053  dvferm2lem  25055  plyeq0lem  25276  logno1  25696  lgsval2lem  26360  pntpbnd2  26640  ubico  30998  bnj1523  32951  sn-inelr  40356  pm2.65ni  42481  lbioc  42941  salgencntex  43772