![]() |
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 2428 pssnn 9170 pssnnOLD 9267 alephadd 10574 axextnd 10588 axunnd 10593 axpownd 10598 axregndlem2 10600 axregnd 10601 axinfndlem1 10602 axinfnd 10603 2cshwcshw 14780 ressress 17197 frgrreg 29914 bj-hbaeb2 35999 hbae-o 38076 hbequid 38082 ax5eq 38105 ax5el 38110 odd2prm2 46684 |
Copyright terms: Public domain | W3C validator |