![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.65i | Structured version Visualization version GIF version |
Description: Inference rule 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 134 | . 2 ⊢ (𝜓 → ¬ 𝜑) |
3 | pm2.65i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
4 | 3 | con3i 150 | . 2 ⊢ (¬ 𝜓 → ¬ 𝜑) |
5 | 2, 4 | pm2.61i 176 | 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 186 mto 188 mt2 191 noel 3952 0nelop 4989 canth 6648 sdom0 8133 canthwdom 8525 cardprclem 8843 ominf4 9172 canthp1lem2 9513 pwfseqlem4 9522 pwxpndom2 9525 lbioo 12244 ubioo 12245 fzp1disj 12437 fzonel 12522 fzouzdisj 12543 hashbclem 13274 harmonic 14635 eirrlem 14976 ruclem13 15015 prmreclem6 15672 4sqlem17 15712 vdwlem12 15743 vdwnnlem3 15748 mreexmrid 16350 psgnunilem3 17962 efgredlemb 18205 efgredlem 18206 00lss 18990 alexsublem 21895 ptcmplem4 21906 nmoleub2lem3 22961 dvferm1lem 23792 dvferm2lem 23794 plyeq0lem 24011 logno1 24427 lgsval2lem 25077 pntpbnd2 25321 ubico 29665 bnj1523 31265 pm2.65ni 39524 lbioc 40057 salgencntex 40879 |
Copyright terms: Public domain | W3C validator |