Theorem syl21anc 1237

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 309	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		syl21anc.4	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  issod  4318  brcogw  4795  funprg  5265  funtpg  5266  fnunsn  5322  ftpg  5699  fsnunf  5715  isotr  5814  off  6092  caofrss  6104  tfr1onlembxssdm  6341  tfrcllembxssdm  6354  pmresg  6673  ac6sfi  6895  tridc  6896  fidcenumlemrks  6949  sbthlemi8  6960  casefun  7081  caseinj  7085  djufun  7100  djuinj  7102  mulclpi  7324  archnqq  7413  addlocprlemlt  7527  addlocprlemeq  7529  addlocprlemgt  7530  mullocprlem  7566  apreim  8556  subrecap  8792  ltrec1  8841  divge0d  9733  fseq1p1m1  10089  q2submod  10380  seq3caopr2  10477  seq3distr  10508  facavg  10719  shftfibg  10822  sqrtdiv  11044  sqrtdivd  11170  mulcn2  11313  demoivreALT  11774  dvdslegcd  11957  gcdnncl  11960  qredeu  12089  rpdvds  12091  rpexp  12145  oddpwdclemodd  12164  divnumden  12188  divdenle  12189  phimullem  12217  phisum  12232  pythagtriplem4  12260  pythagtriplem8  12264  pythagtriplem9  12265  pcgcd1  12319  fldivp1  12338  pockthlem  12346  setsfun  12489  setsfun0  12490  strleund  12554  mndpropd  12773  grpidssd  12878  grpinvssd  12879  issubg2m  12980  isnsg3  12998  eqgid  13016  comet  13870  fsumcncntop  13927  mulcncf  13962  2sqlem8a  14329  2sqlem8  14330  trilpo  14651  neapmkv  14675