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  5434  canth  7295  canthwdom  9460  cardprclem  9864  ominf4  10195  canthp1lem2  10536  pwfseqlem4  10545  pwxpndom2  10548  lbioo  13268  ubioo  13269  fzp1disj  13475  fzonel  13565  fzouzdisj  13587  hashbclem  14351  harmonic  15758  eirrlem  16105  ruclem13  16143  prmreclem6  16825  4sqlem17  16865  vdwlem12  16896  vdwnnlem3  16901  mreexmrid  17541  psgnunilem3  19401  efgredlemb  19651  efgredlem  19652  00lss  20867  alexsublem  23952  ptcmplem4  23963  nmoleub2lem3  25035  dvferm1lem  25908  dvferm2lem  25910  plyeq0lem  26135  logno1  26565  lgsval2lem  27238  pntpbnd2  27518  ubico  32748  bnj1523  35073  antnest  35701  pm2.65ni  45062  lbioc  45532  salgencntex  46360