![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an2i | GIF version |
Description: mp3an 1283 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 1270 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏) |
6 | 1, 2, 5 | syl2anc 406 | 1 ⊢ (𝜓 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 930 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 932 |
This theorem is referenced by: mapen 6669 mapxpen 6671 ctssdclemr 6911 en2eleq 6960 nnledivrp 9394 xsubge0 9505 frec2uzsucd 10015 seq3shft 10451 geolim2 11120 geoisum1c 11128 eflegeo 11206 sin01gt0 11266 cos01gt0 11267 gcdn0gt0 11461 divgcdodd 11614 sqpweven 11645 2sqpwodd 11646 ressid 11802 topnvalg 11914 restbasg 12119 restco 12125 lmfval 12143 cnfval 12145 cnpval 12148 upxp 12222 uptx 12224 txrest 12226 xblm 12345 bdmet 12430 bdmopn 12432 dvidlemap 12533 trilpolemisumle 12815 |
Copyright terms: Public domain | W3C validator |