![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an2i | GIF version |
Description: mp3an 1337 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
Ref | Expression |
---|---|
mp3an2i.1 | ⊢ 𝜑 |
mp3an2i.2 | ⊢ (𝜓 → 𝜒) |
mp3an2i.3 | ⊢ (𝜓 → 𝜃) |
mp3an2i.4 | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
mp3an2i | ⊢ (𝜓 → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an2i.2 | . 2 ⊢ (𝜓 → 𝜒) | |
2 | mp3an2i.3 | . 2 ⊢ (𝜓 → 𝜃) | |
3 | mp3an2i.1 | . . 3 ⊢ 𝜑 | |
4 | mp3an2i.4 | . . 3 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
5 | 3, 4 | mp3an1 1324 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏) |
6 | 1, 2, 5 | syl2anc 411 | 1 ⊢ (𝜓 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: mapen 6845 mapxpen 6847 en2eleq 7193 nnledivrp 9765 xsubge0 9880 iccen 10005 frec2uzsucd 10400 seq3shft 10846 geolim2 11519 geoisum1c 11527 ntrivcvgap 11555 eflegeo 11708 sin01gt0 11768 cos01gt0 11769 gcdn0gt0 11978 uzwodc 12037 divgcdodd 12142 sqpweven 12174 2sqpwodd 12175 pythagtriplem4 12267 pythagtriplem11 12273 pythagtriplem12 12274 pythagtriplem13 12275 pythagtriplem14 12276 pcfac 12347 omctfn 12443 ssnnctlemct 12446 topnvalg 12699 imasmulr 12729 imasaddfnlemg 12734 ismhm 12852 scaffng 13397 zringinvg 13464 restbasg 13638 restco 13644 lmfval 13662 cnfval 13664 cnpval 13668 upxp 13742 uptx 13744 txrest 13746 xblm 13887 bdmet 13972 bdmopn 13974 reopnap 14008 cnopnap 14064 dvidlemap 14130 dvcj 14143 eflt 14166 logdivlti 14272 trilpolemisumle 14756 |
Copyright terms: Public domain | W3C validator |