Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an2i | GIF version |
Description: mp3an 1300 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 1287 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏) |
6 | 1, 2, 5 | syl2anc 408 | 1 ⊢ (𝜓 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: mapen 6708 mapxpen 6710 en2eleq 7019 nnledivrp 9521 xsubge0 9632 frec2uzsucd 10142 seq3shft 10578 geolim2 11249 geoisum1c 11257 eflegeo 11335 sin01gt0 11395 cos01gt0 11396 gcdn0gt0 11593 divgcdodd 11748 sqpweven 11780 2sqpwodd 11781 ressid 11947 topnvalg 12059 restbasg 12264 restco 12270 lmfval 12288 cnfval 12290 cnpval 12294 upxp 12368 uptx 12370 txrest 12372 xblm 12513 bdmet 12598 bdmopn 12600 reopnap 12634 cnopnap 12690 dvidlemap 12756 dvcj 12769 trilpolemisumle 13158 |
Copyright terms: Public domain | W3C validator |