Theorem syl2an2 589

Description: syl2an 287 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 287	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜑)) → 𝜏)
5	4	anabss7 578	1 ⊢ ((𝜒 ∧ 𝜑) → 𝜏)

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  6711  xposdif  9826  qbtwnz  10195  seq3f1o  10447  exp3vallem  10464  fihashf1rn  10710  xrmin2inf  11218  sumrbdclem  11327  summodclem3  11330  zsumdc  11334  fsum3cvg2  11344  mertenslem2  11486  mertensabs  11487  prodrbdclem  11521  prodmodclem2a  11526  zproddc  11529  eftcl  11604  divalgmod  11873  gcdsupex  11899  gcdsupcl  11900  cncongr2  12045  isprm3  12059  eulerthlemrprm  12170  eulerthlema  12171  pcmptdvds  12284  lgsval2lem  13664  nninfself  14006