Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an2i | GIF version |
Description: mp3an 1315 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 1302 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜏) |
6 | 1, 2, 5 | syl2anc 408 | 1 ⊢ (𝜓 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 962 |
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 964 |
This theorem is referenced by: mapen 6740 mapxpen 6742 en2eleq 7051 nnledivrp 9553 xsubge0 9664 frec2uzsucd 10174 seq3shft 10610 geolim2 11281 geoisum1c 11289 ntrivcvgap 11317 eflegeo 11408 sin01gt0 11468 cos01gt0 11469 gcdn0gt0 11666 divgcdodd 11821 sqpweven 11853 2sqpwodd 11854 ressid 12020 topnvalg 12132 restbasg 12337 restco 12343 lmfval 12361 cnfval 12363 cnpval 12367 upxp 12441 uptx 12443 txrest 12445 xblm 12586 bdmet 12671 bdmopn 12673 reopnap 12707 cnopnap 12763 dvidlemap 12829 dvcj 12842 trilpolemisumle 13231 |
Copyright terms: Public domain | W3C validator |