Theorem syl21anc 1270

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  4407  brcogw  4888  funprg  5367  funtpg  5368  fnunsn  5426  fun2d  5495  ftpg  5816  fsnunf  5832  isotr  5933  off  6221  caofrss  6240  tfr1onlembxssdm  6479  tfrcllembxssdm  6492  pmresg  6813  ac6sfi  7048  tridc  7049  tpfidceq  7080  fidcenumlemrks  7108  sbthlemi8  7119  casefun  7240  caseinj  7244  djufun  7259  djuinj  7261  mulclpi  7503  archnqq  7592  addlocprlemlt  7706  addlocprlemeq  7708  addlocprlemgt  7709  mullocprlem  7745  apreim  8738  subrecap  8974  ltrec1  9023  divge0d  9921  fseq1p1m1  10278  q2submod  10594  seq3caopr2  10702  seqcaopr2g  10703  seq3distr  10741  facavg  10955  swrdwrdsymbg  11182  cats1un  11239  shftfibg  11317  sqrtdiv  11539  sqrtdivd  11665  mulcn2  11809  demoivreALT  12271  dvdslegcd  12471  gcdnncl  12474  qredeu  12605  rpdvds  12607  rpexp  12661  oddpwdclemodd  12680  divnumden  12704  divdenle  12705  phimullem  12733  phisum  12749  pythagtriplem4  12777  pythagtriplem8  12781  pythagtriplem9  12782  pcgcd1  12837  fldivp1  12857  pockthlem  12865  setsfun  13053  setsfun0  13054  strleund  13122  ercpbl  13350  sgrppropd  13432  mndpropd  13459  grpidssd  13595  grpinvssd  13596  issubg2m  13712  isnsg3  13730  eqgid  13749  kerf1ghm  13797  lmodprop2d  14297  lsspropdg  14380  znidomb  14607  znrrg  14609  comet  15158  fsumcncntop  15226  mulcncf  15267  mpodvdsmulf1o  15649  gausslemma2dlem0d  15716  gausslemma2dlem1a  15722  2lgslem1a1  15750  2sqlem8a  15786  2sqlem8  15787  trilpo  16342  neapmkv  16367