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  5436  canth  7300  canthwdom  9465  cardprclem  9869  ominf4  10200  canthp1lem2  10541  pwfseqlem4  10550  pwxpndom2  10553  lbioo  13273  ubioo  13274  fzp1disj  13480  fzonel  13570  fzouzdisj  13592  hashbclem  14356  harmonic  15763  eirrlem  16110  ruclem13  16148  prmreclem6  16830  4sqlem17  16870  vdwlem12  16901  vdwnnlem3  16906  mreexmrid  17546  psgnunilem3  19406  efgredlemb  19656  efgredlem  19657  00lss  20872  alexsublem  23957  ptcmplem4  23968  nmoleub2lem3  25040  dvferm1lem  25913  dvferm2lem  25915  plyeq0lem  26140  logno1  26570  lgsval2lem  27243  pntpbnd2  27523  ubico  32753  bnj1523  35078  antnest  35721  pm2.65ni  45082  lbioc  45552  salgencntex  46380