Theorem syl12anc 1276

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

Hypotheses

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

Assertion

Ref	Expression
syl12anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl12anc

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  syl22anc  1279  cocan1  5996  fliftfun  6005  isopolem  6031  f1oiso2  6036  caovcld  6246  caovcomd  6249  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  1dom1el  7112  fidceq  7176  findcard2d  7200  diffifi  7203  tridc  7209  en2eqpr  7219  sbthlemi9  7288  supisolem  7355  ordiso2  7382  difinfsnlem  7446  difinfsn  7447  pr2cv1  7548  prarloclemup  7869  prarloc  7877  nqprl  7925  nqpru  7926  ltaddpr  7971  aptiprlemu  8014  archpr  8017  cauappcvgprlem2  8034  caucvgprlem2  8054  caucvgprprlem2  8084  suplocexprlemlub  8098  suplocexpr  8099  recexgt0sr  8147  archsr  8156  axpre-suploclemres  8275  conjmulap  9068  lerec2  9228  ledivp1  9242  cju  9300  nn2ge  9347  gtndiv  9753  supinfneg  10012  infsupneg  10013  z2ge  10246  iccssioo2  10366  fzrev3  10512  elfz1b  10515  zsupcllemstep  10680  zsupssdc  10691  exbtwnzlemstep  10700  exbtwnzlemex  10702  rebtwn2zlemstep  10705  rebtwn2z  10707  qbtwnre  10709  flqdiv  10780  frec2uzled  10888  seq3caopr  10954  seqcaoprg  10955  iseqf1olemab  10961  iseqf1olemnanb  10962  seqf1oglem1  10978  expnegzap  11032  nn0ltexp2  11170  hashen  11246  hashunlem  11267  hashprg  11272  hashfibclem  11305  hashf1lem2  11309  leisorel  11312  zfz1isolemiso  11314  seq3coll  11317  swrdccat3b  11535  caucvgrelemrec  11768  resqrexlemex  11814  minmax  12021  xrminmax  12057  fsum2dlemstep  12227  fisumcom2  12231  zproddc  12372  fprod2dlemstep  12415  fprodcom2fi  12419  bezoutlemmain  12801  sqgcd  12832  pcpremul  13102  pceulem  13103  pceu  13104  pczpre  13106  pcdiv  13111  pcqmul  13112  pcqdiv  13116  pcexp  13118  pcdvdsb  13129  pcneg  13134  pcdvdstr  13136  pcgcd1  13137  pc2dvds  13139  pcz  13141  pcaddlem  13148  pcadd  13149  qexpz  13161  expnprm  13162  infpnlem2  13169  ballotfilemfc0  13291  ballotfilemfcc  13292  f1ocpbllem  13691  f1ovscpbl  13693  sgrppropd  13788  mndpropd  13813  grpsubpropd2  13970  f1ghm0to0  14135  ablnnncan  14218  rngpropd  14362  ringpropd  14451  lmodprop2d  14795  lsspropdg  14878  assapropd  15124  neiint  15383  restbasg  15406  iscnp4  15456  cnconst2  15471  cnpdis  15480  neitx  15506  upxp  15510  hmeoimaf1o  15552  blssexps  15667  blssex  15668  ssblex  15669  bdmopn  15742  xmettx  15748  metcnp3  15749  tgioo  15792  tgqioo  15793  dvmptfsum  15963  elply2  15973  sin0pilem2  16021  logbgcd1irr  16215  perfect  16313  bposlem2  16324  lgsval  16340  lgsfcl2  16342  lgsdir  16371  lgsdilem2  16372  lgsdi  16373  lgsne0  16374  clwwlknonex2e  16898  pwle2  17245  qdiff  17317