![]() |
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 181 | . 2 ⊢ (¬ 𝜑 → 𝜒) |
5 | 1, 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.61iii 185 hbae 2431 pssnn 9168 pssnnOLD 9265 alephadd 10572 axextnd 10586 axunnd 10591 axpownd 10596 axregndlem2 10598 axregnd 10599 axinfndlem1 10600 axinfnd 10601 2cshwcshw 14776 ressress 17193 frgrreg 29647 bj-hbaeb2 35696 hbae-o 37773 hbequid 37779 ax5eq 37802 ax5el 37807 odd2prm2 46386 |
Copyright terms: Public domain | W3C validator |