Theorem syl12anc 1247

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  1250  cocan1  5837  fliftfun  5846  isopolem  5872  f1oiso2  5877  caovcld  6081  caovcomd  6084  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  fidceq  6939  findcard2d  6961  diffifi  6964  tridc  6969  en2eqpr  6977  sbthlemi9  7040  supisolem  7083  ordiso2  7110  difinfsnlem  7174  difinfsn  7175  prarloclemup  7579  prarloc  7587  nqprl  7635  nqpru  7636  ltaddpr  7681  aptiprlemu  7724  archpr  7727  cauappcvgprlem2  7744  caucvgprlem2  7764  caucvgprprlem2  7794  suplocexprlemlub  7808  suplocexpr  7809  recexgt0sr  7857  archsr  7866  axpre-suploclemres  7985  conjmulap  8773  lerec2  8933  ledivp1  8947  cju  9005  nn2ge  9040  gtndiv  9438  supinfneg  9686  infsupneg  9687  z2ge  9918  iccssioo2  10038  fzrev3  10179  elfz1b  10182  zsupcllemstep  10336  zsupssdc  10345  exbtwnzlemstep  10354  exbtwnzlemex  10356  rebtwn2zlemstep  10359  rebtwn2z  10361  qbtwnre  10363  flqdiv  10430  frec2uzled  10538  seq3caopr  10604  seqcaoprg  10605  iseqf1olemab  10611  iseqf1olemnanb  10612  seqf1oglem1  10628  expnegzap  10682  nn0ltexp2  10818  hashen  10893  hashunlem  10913  hashprg  10917  leisorel  10946  zfz1isolemiso  10948  seq3coll  10951  caucvgrelemrec  11161  resqrexlemex  11207  minmax  11412  xrminmax  11447  fsum2dlemstep  11616  fisumcom2  11620  zproddc  11761  fprod2dlemstep  11804  fprodcom2fi  11808  bezoutlemmain  12190  sqgcd  12221  pcpremul  12487  pceulem  12488  pceu  12489  pczpre  12491  pcdiv  12496  pcqmul  12497  pcqdiv  12501  pcexp  12503  pcdvdsb  12514  pcneg  12519  pcdvdstr  12521  pcgcd1  12522  pc2dvds  12524  pcz  12526  pcaddlem  12533  pcadd  12534  qexpz  12546  expnprm  12547  infpnlem2  12554  f1ocpbllem  13012  f1ovscpbl  13014  sgrppropd  13115  mndpropd  13142  grpsubpropd2  13307  f1ghm0to0  13478  ablnnncan  13529  rngpropd  13587  ringpropd  13670  lmodprop2d  13980  lsspropdg  14063  neiint  14465  restbasg  14488  iscnp4  14538  cnconst2  14553  cnpdis  14562  neitx  14588  upxp  14592  hmeoimaf1o  14634  blssexps  14749  blssex  14750  ssblex  14751  bdmopn  14824  xmettx  14830  metcnp3  14831  tgioo  14874  tgqioo  14875  dvmptfsum  15045  elply2  15055  sin0pilem2  15102  logbgcd1irr  15287  perfect  15321  lgsval  15329  lgsfcl2  15331  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  1dom1el  15721  pwle2  15729