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 ⊢ (𝜑 → 𝜏)

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:  syl22anc  1279  cocan1  5987  fliftfun  5996  isopolem  6022  f1oiso2  6027  caovcld  6237  caovcomd  6240  tfrlemisucaccv  6590  tfr1onlemsucaccv  6606  tfr1onlembxssdm  6608  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  1dom1el  7101  fidceq  7165  findcard2d  7189  diffifi  7192  tridc  7198  en2eqpr  7208  sbthlemi9  7276  supisolem  7342  ordiso2  7369  difinfsnlem  7433  difinfsn  7434  pr2cv1  7535  prarloclemup  7856  prarloc  7864  nqprl  7912  nqpru  7913  ltaddpr  7958  aptiprlemu  8001  archpr  8004  cauappcvgprlem2  8021  caucvgprlem2  8041  caucvgprprlem2  8071  suplocexprlemlub  8085  suplocexpr  8086  recexgt0sr  8134  archsr  8143  axpre-suploclemres  8262  conjmulap  9053  lerec2  9213  ledivp1  9227  cju  9285  nn2ge  9320  gtndiv  9724  supinfneg  9978  infsupneg  9979  z2ge  10211  iccssioo2  10331  fzrev3  10477  elfz1b  10480  zsupcllemstep  10645  zsupssdc  10656  exbtwnzlemstep  10665  exbtwnzlemex  10667  rebtwn2zlemstep  10670  rebtwn2z  10672  qbtwnre  10674  flqdiv  10741  frec2uzled  10849  seq3caopr  10915  seqcaoprg  10916  iseqf1olemab  10922  iseqf1olemnanb  10923  seqf1oglem1  10939  expnegzap  10993  nn0ltexp2  11130  hashen  11206  hashunlem  11227  hashprg  11232  hashfibclem  11265  hashf1lem2  11269  leisorel  11272  zfz1isolemiso  11274  seq3coll  11277  swrdccat3b  11495  caucvgrelemrec  11728  resqrexlemex  11774  minmax  11979  xrminmax  12014  fsum2dlemstep  12184  fisumcom2  12188  zproddc  12329  fprod2dlemstep  12372  fprodcom2fi  12376  bezoutlemmain  12758  sqgcd  12789  pcpremul  13055  pceulem  13056  pceu  13057  pczpre  13059  pcdiv  13064  pcqmul  13065  pcqdiv  13069  pcexp  13071  pcdvdsb  13082  pcneg  13087  pcdvdstr  13089  pcgcd1  13090  pc2dvds  13092  pcz  13094  pcaddlem  13101  pcadd  13102  qexpz  13114  expnprm  13115  infpnlem2  13122  ballotfilemfc0  13215  ballotfilemfcc  13216  f1ocpbllem  13614  f1ovscpbl  13616  sgrppropd  13711  mndpropd  13736  grpsubpropd2  13893  f1ghm0to0  14058  ablnnncan  14110  rngpropd  14237  ringpropd  14326  lmodprop2d  14668  lsspropdg  14751  assapropd  14997  neiint  15229  restbasg  15252  iscnp4  15302  cnconst2  15317  cnpdis  15326  neitx  15352  upxp  15356  hmeoimaf1o  15398  blssexps  15513  blssex  15514  ssblex  15515  bdmopn  15588  xmettx  15594  metcnp3  15595  tgioo  15638  tgqioo  15639  dvmptfsum  15809  elply2  15819  sin0pilem2  15866  logbgcd1irr  16052  perfect  16098  lgsval  16106  lgsfcl2  16108  lgsdir  16137  lgsdilem2  16138  lgsdi  16139  lgsne0  16140  clwwlknonex2e  16664  pwle2  17011  qdiff  17072