Theorem syl21anc 1226

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  4291  brcogw  4767  funprg  5232  funtpg  5233  fnunsn  5289  ftpg  5663  fsnunf  5679  isotr  5778  off  6056  caofrss  6068  tfr1onlembxssdm  6302  tfrcllembxssdm  6315  pmresg  6633  ac6sfi  6855  tridc  6856  fidcenumlemrks  6909  sbthlemi8  6920  casefun  7041  caseinj  7045  djufun  7060  djuinj  7062  mulclpi  7260  archnqq  7349  addlocprlemlt  7463  addlocprlemeq  7465  addlocprlemgt  7466  mullocprlem  7502  apreim  8492  subrecap  8726  ltrec1  8774  divge0d  9664  fseq1p1m1  10019  q2submod  10310  seq3caopr2  10407  seq3distr  10438  facavg  10648  shftfibg  10748  sqrtdiv  10970  sqrtdivd  11096  mulcn2  11239  demoivreALT  11700  dvdslegcd  11882  gcdnncl  11885  qredeu  12008  rpdvds  12010  rpexp  12062  oddpwdclemodd  12081  divnumden  12105  divdenle  12106  phimullem  12134  phisum  12149  pythagtriplem4  12177  pythagtriplem8  12181  pythagtriplem9  12182  pcgcd1  12236  fldivp1  12255  setsfun  12366  setsfun0  12367  strleund  12419  comet  13040  fsumcncntop  13097  mulcncf  13132  trilpo  13756  neapmkv  13780