| 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 139 | . 2 ⊢ (𝜓 → ¬ 𝜑) |
| 3 | pm2.65i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 4 | 3 | con3i 154 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜑) |
| 5 | 2, 4 | pm2.61i 182 | 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 195 mto 197 mt2 200 0nelop 5444 canth 7312 canthwdom 9484 cardprclem 9891 ominf4 10222 canthp1lem2 10564 pwfseqlem4 10573 pwxpndom2 10576 lbioo 13292 ubioo 13293 fzp1disj 13499 fzonel 13589 fzouzdisj 13611 hashbclem 14375 harmonic 15782 eirrlem 16129 ruclem13 16167 prmreclem6 16849 4sqlem17 16889 vdwlem12 16920 vdwnnlem3 16925 mreexmrid 17566 psgnunilem3 19425 efgredlemb 19675 efgredlem 19676 00lss 20892 alexsublem 23988 ptcmplem4 23999 nmoleub2lem3 25071 dvferm1lem 25944 dvferm2lem 25946 plyeq0lem 26171 logno1 26601 lgsval2lem 27274 pntpbnd2 27554 ubico 32855 bnj1523 35227 antnest 35883 pm2.65ni 45287 lbioc 45755 salgencntex 46583 |
| Copyright terms: Public domain | W3C validator |