![]() |
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 194 mto 196 mt2 199 0nelop 5498 canth 7372 sdom0OLD 9134 canthwdom 9604 cardprclem 10004 ominf4 10337 canthp1lem2 10678 pwfseqlem4 10687 pwxpndom2 10690 lbioo 13390 ubioo 13391 fzp1disj 13595 fzonel 13681 fzouzdisj 13703 hashbclem 14447 harmonic 15841 eirrlem 16184 ruclem13 16222 prmreclem6 16893 4sqlem17 16933 vdwlem12 16964 vdwnnlem3 16969 mreexmrid 17626 psgnunilem3 19463 efgredlemb 19713 efgredlem 19714 00lss 20837 alexsublem 23992 ptcmplem4 24003 nmoleub2lem3 25086 dvferm1lem 25960 dvferm2lem 25962 plyeq0lem 26189 logno1 26615 lgsval2lem 27285 pntpbnd2 27565 ubico 32625 bnj1523 34833 sn-inelr 42155 pm2.65ni 44550 lbioc 45036 salgencntex 45869 |
Copyright terms: Public domain | W3C validator |