Theorem syl2an2 602

Description: syl2an 289 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)

Hypotheses

Ref	Expression
syl2an2.1	⊢ (𝜑 → 𝜓)
syl2an2.2	⊢ ((𝜒 ∧ 𝜑) → 𝜃)
syl2an2.3	⊢ ((𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl2an2	⊢ ((𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem 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 589	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mapsnf1o  7024  fcdmnn0fsuppg  9630  xposdif  10302  qbtwnz  10704  seq3f1o  10976  exp3vallem  10999  fihashf1rn  11250  fun2dmnop0  11325  xrmin2inf  12060  sumrbdclem  12170  summodclem3  12173  zsumdc  12177  fsum3cvg2  12187  mertenslem2  12329  mertensabs  12330  prodrbdclem  12364  prodmodclem2a  12369  zproddc  12372  eftcl  12447  divalgmod  12720  bitsmod  12749  gcdsupex  12760  gcdsupcl  12761  cncongr2  12908  isprm3  12922  eulerthlemrprm  13037  eulerthlema  13038  pcmptdvds  13154  idjufi  14270  prdsex  14280  elplyd  15979  ply1term  15981  zprmlogbaplem3  16229  lgsval2lem  16346  nninfself  17274