Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl2an2 | GIF version |
Description: syl2an 287 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 287 | . 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜑)) → 𝜏) |
5 | 4 | anabss7 572 | 1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
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 |
This theorem is referenced by: mapsnf1o 6631 xposdif 9665 qbtwnz 10029 seq3f1o 10277 exp3vallem 10294 fihashf1rn 10535 xrmin2inf 11037 sumrbdclem 11146 summodclem3 11149 zsumdc 11153 fsum3cvg2 11163 mertenslem2 11305 mertensabs 11306 prodrbdclem 11340 prodmodclem2a 11345 eftcl 11360 divalgmod 11624 gcdsupex 11646 gcdsupcl 11647 cncongr2 11785 isprm3 11799 nninfself 13209 |
Copyright terms: Public domain | W3C validator |