![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.65i | Structured version Visualization version GIF version |
Description: Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Ref | Expression |
---|---|
pm2.65i.1 | ⊢ (𝜑 → 𝜓) |
pm2.65i.2 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
pm2.65i | ⊢ ¬ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.65i.2 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
2 | 1 | con2i 137 | . 2 ⊢ (𝜓 → ¬ 𝜑) |
3 | pm2.65i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
4 | 3 | con3i 152 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜑) |
5 | 2, 4 | pm2.61i 177 | 1 ⊢ ¬ 𝜑 |
Colors of variables: wff setvar class |
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 187 mto 189 mt2 192 noelOLD 4147 0nelop 5193 canth 6882 sdom0 8382 canthwdom 8775 cardprclem 9140 ominf4 9471 canthp1lem2 9812 pwfseqlem4 9821 pwxpndom2 9824 lbioo 12522 ubioo 12523 fzp1disj 12721 fzonel 12806 fzouzdisj 12827 hashbclem 13554 harmonic 14999 eirrlem 15340 ruclem13 15379 prmreclem6 16033 4sqlem17 16073 vdwlem12 16104 vdwnnlem3 16109 mreexmrid 16693 psgnunilem3 18304 efgredlemb 18548 efgredlem 18549 efgredlemOLD 18550 00lss 19338 alexsublem 22260 ptcmplem4 22271 nmoleub2lem3 23326 dvferm1lem 24188 dvferm2lem 24190 plyeq0lem 24407 logno1 24823 lgsval2lem 25488 pntpbnd2 25732 ubico 30105 bnj1523 31742 pm2.65ni 40152 lbioc 40658 salgencntex 41495 |
Copyright terms: Public domain | W3C validator |