![]() |
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 6846 mapxpen 6848 en2eleq 7194 nnledivrp 9766 xsubge0 9881 iccen 10006 frec2uzsucd 10401 seq3shft 10847 geolim2 11520 geoisum1c 11528 ntrivcvgap 11556 eflegeo 11709 sin01gt0 11769 cos01gt0 11770 gcdn0gt0 11979 uzwodc 12038 divgcdodd 12143 sqpweven 12175 2sqpwodd 12176 pythagtriplem4 12268 pythagtriplem11 12274 pythagtriplem12 12275 pythagtriplem13 12276 pythagtriplem14 12277 pcfac 12348 omctfn 12444 ssnnctlemct 12447 topnvalg 12700 imasmulr 12730 imasaddfnlemg 12735 ismhm 12853 scaffng 13399 zringinvg 13497 restbasg 13671 restco 13677 lmfval 13695 cnfval 13697 cnpval 13701 upxp 13775 uptx 13777 txrest 13779 xblm 13920 bdmet 14005 bdmopn 14007 reopnap 14041 cnopnap 14097 dvidlemap 14163 dvcj 14176 eflt 14199 logdivlti 14305 trilpolemisumle 14789 |
Copyright terms: Public domain | W3C validator |