| 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 5434 canth 7295 canthwdom 9460 cardprclem 9864 ominf4 10195 canthp1lem2 10536 pwfseqlem4 10545 pwxpndom2 10548 lbioo 13268 ubioo 13269 fzp1disj 13475 fzonel 13565 fzouzdisj 13587 hashbclem 14351 harmonic 15758 eirrlem 16105 ruclem13 16143 prmreclem6 16825 4sqlem17 16865 vdwlem12 16896 vdwnnlem3 16901 mreexmrid 17541 psgnunilem3 19401 efgredlemb 19651 efgredlem 19652 00lss 20867 alexsublem 23952 ptcmplem4 23963 nmoleub2lem3 25035 dvferm1lem 25908 dvferm2lem 25910 plyeq0lem 26135 logno1 26565 lgsval2lem 27238 pntpbnd2 27518 ubico 32748 bnj1523 35073 antnest 35701 pm2.65ni 45062 lbioc 45532 salgencntex 46360 |
| Copyright terms: Public domain | W3C validator |