![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl2an2 | GIF version |
Description: syl2an 285 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 285 | . 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜑)) → 𝜏) |
5 | 4 | anabss7 555 | 1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
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 |
This theorem is referenced by: mapsnf1o 6583 xposdif 9552 qbtwnz 9916 seq3f1o 10164 exp3vallem 10181 fihashf1rn 10422 xrmin2inf 10923 sumrbdclem 11031 summodclem3 11035 zsumdc 11039 fsum3cvg2 11049 mertenslem2 11191 mertensabs 11192 eftcl 11205 divalgmod 11466 gcdsupex 11488 gcdsupcl 11489 cncongr2 11625 isprm3 11639 nninfself 12890 |
Copyright terms: Public domain | W3C validator |