![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl2an2 | GIF version |
Description: syl2an 289 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
Ref | Expression |
---|---|
syl2an2.1 | ⊢ (𝜑 → 𝜓) |
syl2an2.2 | ⊢ ((𝜒 ∧ 𝜑) → 𝜃) |
syl2an2.3 | ⊢ ((𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl2an2 | ⊢ ((𝜒 ∧ 𝜑) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an2.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl2an2.2 | . . 3 ⊢ ((𝜒 ∧ 𝜑) → 𝜃) | |
3 | syl2an2.3 | . . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏) | |
4 | 1, 2, 3 | syl2an 289 | . 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜑)) → 𝜏) |
5 | 4 | anabss7 583 | 1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
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 |
This theorem is referenced by: mapsnf1o 6751 xposdif 9896 qbtwnz 10266 seq3f1o 10518 exp3vallem 10535 fihashf1rn 10782 xrmin2inf 11290 sumrbdclem 11399 summodclem3 11402 zsumdc 11406 fsum3cvg2 11416 mertenslem2 11558 mertensabs 11559 prodrbdclem 11593 prodmodclem2a 11598 zproddc 11601 eftcl 11676 divalgmod 11946 gcdsupex 11972 gcdsupcl 11973 cncongr2 12118 isprm3 12132 eulerthlemrprm 12243 eulerthlema 12244 pcmptdvds 12357 prdsex 12736 lgsval2lem 14707 nninfself 15059 |
Copyright terms: Public domain | W3C validator |