![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an2i | GIF version |
Description: mp3an 1348 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 1335 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏) |
6 | 1, 2, 5 | syl2anc 411 | 1 ⊢ (𝜓 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 |
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 982 |
This theorem is referenced by: mapen 6874 mapxpen 6876 en2eleq 7224 nnledivrp 9796 xsubge0 9911 iccen 10036 frec2uzsucd 10432 seq3shft 10879 geolim2 11552 geoisum1c 11560 ntrivcvgap 11588 eflegeo 11741 sin01gt0 11801 cos01gt0 11802 gcdn0gt0 12011 uzwodc 12070 divgcdodd 12175 sqpweven 12207 2sqpwodd 12208 pythagtriplem4 12300 pythagtriplem11 12306 pythagtriplem12 12307 pythagtriplem13 12308 pythagtriplem14 12309 pcfac 12382 4sqlemffi 12428 omctfn 12494 ssnnctlemct 12497 topnvalg 12756 imasmulr 12786 imasaddfnlemg 12791 ismhm 12913 mhmex 12914 scaffng 13625 lss1d 13699 zringinvg 13903 restbasg 14125 restco 14131 lmfval 14149 cnfval 14151 cnpval 14155 upxp 14229 uptx 14231 txrest 14233 xblm 14374 bdmet 14459 bdmopn 14461 reopnap 14495 cnopnap 14551 dvidlemap 14617 dvcj 14630 eflt 14653 logdivlti 14759 trilpolemisumle 15245 |
Copyright terms: Public domain | W3C validator |