Theorem syl12anc 1250

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  1253  cocan1  5884  fliftfun  5893  isopolem  5919  f1oiso2  5924  caovcld  6130  caovcomd  6133  tfrlemisucaccv  6441  tfr1onlemsucaccv  6457  tfr1onlembxssdm  6459  tfrcllemsucaccv  6470  tfrcllembxssdm  6472  fidceq  6999  findcard2d  7021  diffifi  7024  tridc  7029  en2eqpr  7037  sbthlemi9  7100  supisolem  7143  ordiso2  7170  difinfsnlem  7234  difinfsn  7235  pr2cv1  7336  prarloclemup  7650  prarloc  7658  nqprl  7706  nqpru  7707  ltaddpr  7752  aptiprlemu  7795  archpr  7798  cauappcvgprlem2  7815  caucvgprlem2  7835  caucvgprprlem2  7865  suplocexprlemlub  7879  suplocexpr  7880  recexgt0sr  7928  archsr  7937  axpre-suploclemres  8056  conjmulap  8844  lerec2  9004  ledivp1  9018  cju  9076  nn2ge  9111  gtndiv  9510  supinfneg  9758  infsupneg  9759  z2ge  9990  iccssioo2  10110  fzrev3  10251  elfz1b  10254  zsupcllemstep  10416  zsupssdc  10425  exbtwnzlemstep  10434  exbtwnzlemex  10436  rebtwn2zlemstep  10439  rebtwn2z  10441  qbtwnre  10443  flqdiv  10510  frec2uzled  10618  seq3caopr  10684  seqcaoprg  10685  iseqf1olemab  10691  iseqf1olemnanb  10692  seqf1oglem1  10708  expnegzap  10762  nn0ltexp2  10898  hashen  10973  hashunlem  10993  hashprg  10997  leisorel  11026  zfz1isolemiso  11028  seq3coll  11031  swrdccat3b  11238  caucvgrelemrec  11456  resqrexlemex  11502  minmax  11707  xrminmax  11742  fsum2dlemstep  11911  fisumcom2  11915  zproddc  12056  fprod2dlemstep  12099  fprodcom2fi  12103  bezoutlemmain  12485  sqgcd  12516  pcpremul  12782  pceulem  12783  pceu  12784  pczpre  12786  pcdiv  12791  pcqmul  12792  pcqdiv  12796  pcexp  12798  pcdvdsb  12809  pcneg  12814  pcdvdstr  12816  pcgcd1  12817  pc2dvds  12819  pcz  12821  pcaddlem  12828  pcadd  12829  qexpz  12841  expnprm  12842  infpnlem2  12849  f1ocpbllem  13309  f1ovscpbl  13311  sgrppropd  13412  mndpropd  13439  grpsubpropd2  13604  f1ghm0to0  13775  ablnnncan  13826  rngpropd  13884  ringpropd  13967  lmodprop2d  14277  lsspropdg  14360  neiint  14784  restbasg  14807  iscnp4  14857  cnconst2  14872  cnpdis  14881  neitx  14907  upxp  14911  hmeoimaf1o  14953  blssexps  15068  blssex  15069  ssblex  15070  bdmopn  15143  xmettx  15149  metcnp3  15150  tgioo  15193  tgqioo  15194  dvmptfsum  15364  elply2  15374  sin0pilem2  15421  logbgcd1irr  15606  perfect  15640  lgsval  15648  lgsfcl2  15650  lgsdir  15679  lgsdilem2  15680  lgsdi  15681  lgsne0  15682  1dom1el  16264  pwle2  16275