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  5497  canth  7362  sdom0OLD  9109  canthwdom  9574  cardprclem  9974  ominf4  10307  canthp1lem2  10648  pwfseqlem4  10657  pwxpndom2  10660  lbioo  13355  ubioo  13356  fzp1disj  13560  fzonel  13646  fzouzdisj  13668  hashbclem  14411  harmonic  15805  eirrlem  16147  ruclem13  16185  prmreclem6  16854  4sqlem17  16894  vdwlem12  16925  vdwnnlem3  16930  mreexmrid  17587  psgnunilem3  19364  efgredlemb  19614  efgredlem  19615  00lss  20552  alexsublem  23548  ptcmplem4  23559  nmoleub2lem3  24631  dvferm1lem  25501  dvferm2lem  25503  plyeq0lem  25724  logno1  26144  lgsval2lem  26810  pntpbnd2  27090  ubico  31986  bnj1523  34082  sn-inelr  41338  pm2.65ni  43731  lbioc  44226  salgencntex  45059