Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm2.61ii | Structured version Visualization version GIF version |
Description: Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
Ref | Expression |
---|---|
pm2.61ii.1 | ⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) |
pm2.61ii.2 | ⊢ (𝜑 → 𝜒) |
pm2.61ii.3 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
pm2.61ii | ⊢ 𝜒 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61ii.2 | . 2 ⊢ (𝜑 → 𝜒) | |
2 | pm2.61ii.1 | . . 3 ⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) | |
3 | pm2.61ii.3 | . . 3 ⊢ (𝜓 → 𝜒) | |
4 | 2, 3 | pm2.61d2 184 | . 2 ⊢ (¬ 𝜑 → 𝜒) |
5 | 1, 4 | pm2.61i 185 | 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.61iii 188 hbae 2430 pssnn 8846 pssnnOLD 8895 alephadd 10191 axextnd 10205 axunnd 10210 axpownd 10215 axregndlem2 10217 axregnd 10218 axinfndlem1 10219 axinfnd 10220 2cshwcshw 14390 ressress 16799 frgrreg 28477 bj-hbaeb2 34738 hbae-o 36654 hbequid 36660 ax5eq 36683 ax5el 36688 odd2prm2 44843 |
Copyright terms: Public domain | W3C validator |