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  5459  canth  7344  canthwdom  9539  cardprclem  9939  ominf4  10272  canthp1lem2  10613  pwfseqlem4  10622  pwxpndom2  10625  lbioo  13344  ubioo  13345  fzp1disj  13551  fzonel  13641  fzouzdisj  13663  hashbclem  14424  harmonic  15832  eirrlem  16179  ruclem13  16217  prmreclem6  16899  4sqlem17  16939  vdwlem12  16970  vdwnnlem3  16975  mreexmrid  17611  psgnunilem3  19433  efgredlemb  19683  efgredlem  19684  00lss  20854  alexsublem  23938  ptcmplem4  23949  nmoleub2lem3  25022  dvferm1lem  25895  dvferm2lem  25897  plyeq0lem  26122  logno1  26552  lgsval2lem  27225  pntpbnd2  27505  ubico  32705  bnj1523  35068  antnest  35683  pm2.65ni  45047  lbioc  45518  salgencntex  46348