Theorem syl21anc 1215

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

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

Assertion

Ref	Expression
syl21anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	jca31 307	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		syl21anc.4	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  issod  4241  brcogw  4708  funprg  5173  funtpg  5174  fnunsn  5230  ftpg  5604  fsnunf  5620  isotr  5717  off  5994  caofrss  6006  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  pmresg  6570  ac6sfi  6792  tridc  6793  fidcenumlemrks  6841  sbthlemi8  6852  casefun  6970  caseinj  6974  djufun  6989  djuinj  6991  mulclpi  7136  archnqq  7225  addlocprlemlt  7339  addlocprlemeq  7341  addlocprlemgt  7342  mullocprlem  7378  apreim  8365  subrecap  8598  ltrec1  8646  divge0d  9524  fseq1p1m1  9874  q2submod  10158  seq3caopr2  10255  seq3distr  10286  facavg  10492  shftfibg  10592  sqrtdiv  10814  sqrtdivd  10940  mulcn2  11081  demoivreALT  11480  dvdslegcd  11653  gcdnncl  11656  qredeu  11778  rpdvds  11780  rpexp  11831  oddpwdclemodd  11850  divnumden  11874  divdenle  11875  phimullem  11901  setsfun  11994  setsfun0  11995  strleund  12047  comet  12668  fsumcncntop  12725  mulcncf  12760  trilpo  13236