Theorem pm2.65i 194

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  195  mto  197  mt2  200  0nelop  5515  canth  7401  sdom0OLD  9175  canthwdom  9648  cardprclem  10048  ominf4  10381  canthp1lem2  10722  pwfseqlem4  10731  pwxpndom2  10734  lbioo  13438  ubioo  13439  fzp1disj  13643  fzonel  13730  fzouzdisj  13752  hashbclem  14501  harmonic  15907  eirrlem  16252  ruclem13  16290  prmreclem6  16968  4sqlem17  17008  vdwlem12  17039  vdwnnlem3  17044  mreexmrid  17701  psgnunilem3  19538  efgredlemb  19788  efgredlem  19789  00lss  20962  alexsublem  24073  ptcmplem4  24084  nmoleub2lem3  25167  dvferm1lem  26042  dvferm2lem  26044  plyeq0lem  26269  logno1  26696  lgsval2lem  27369  pntpbnd2  27649  ubico  32780  bnj1523  35047  sn-inelr  42443  pm2.65ni  44946  lbioc  45431  salgencntex  46264