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  5456  canth  7341  canthwdom  9532  cardprclem  9932  ominf4  10265  canthp1lem2  10606  pwfseqlem4  10615  pwxpndom2  10618  lbioo  13337  ubioo  13338  fzp1disj  13544  fzonel  13634  fzouzdisj  13656  hashbclem  14417  harmonic  15825  eirrlem  16172  ruclem13  16210  prmreclem6  16892  4sqlem17  16932  vdwlem12  16963  vdwnnlem3  16968  mreexmrid  17604  psgnunilem3  19426  efgredlemb  19676  efgredlem  19677  00lss  20847  alexsublem  23931  ptcmplem4  23942  nmoleub2lem3  25015  dvferm1lem  25888  dvferm2lem  25890  plyeq0lem  26115  logno1  26545  lgsval2lem  27218  pntpbnd2  27498  ubico  32698  bnj1523  35061  antnest  35676  pm2.65ni  45040  lbioc  45511  salgencntex  46341