Theorem pm2.65i 197

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 141	. 2 ⊢ (𝜓 → ¬ 𝜑)
3		pm2.65i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	3	con3i 157	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
5	2, 4	pm2.61i 185	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  198  mto  200  mt2  203  0nelop  5379  canth  7167  sdom0  8778  canthwdom  9195  cardprclem  9595  ominf4  9926  canthp1lem2  10267  pwfseqlem4  10276  pwxpndom2  10279  lbioo  12966  ubioo  12967  fzp1disj  13171  fzonel  13256  fzouzdisj  13278  hashbclem  14016  harmonic  15423  eirrlem  15765  ruclem13  15803  prmreclem6  16474  4sqlem17  16514  vdwlem12  16545  vdwnnlem3  16550  mreexmrid  17146  psgnunilem3  18888  efgredlemb  19136  efgredlem  19137  00lss  19978  alexsublem  22941  ptcmplem4  22952  nmoleub2lem3  24012  dvferm1lem  24881  dvferm2lem  24883  plyeq0lem  25104  logno1  25524  lgsval2lem  26188  pntpbnd2  26468  ubico  30816  bnj1523  32764  sn-inelr  40143  pm2.65ni  42265  lbioc  42726  salgencntex  43557