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  7581  prarloc  7589  nqprl  7637  nqpru  7638  ltaddpr  7683  aptiprlemu  7726  archpr  7729  cauappcvgprlem2  7746  caucvgprlem2  7766  caucvgprprlem2  7796  suplocexprlemlub  7810  suplocexpr  7811  recexgt0sr  7859  archsr  7868  axpre-suploclemres  7987  conjmulap  8775  lerec2  8935  ledivp1  8949  cju  9007  nn2ge  9042  gtndiv  9440  supinfneg  9688  infsupneg  9689  z2ge  9920  iccssioo2  10040  fzrev3  10181  elfz1b  10184  zsupcllemstep  10338  zsupssdc  10347  exbtwnzlemstep  10356  exbtwnzlemex  10358  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnre  10365  flqdiv  10432  frec2uzled  10540  seq3caopr  10606  seqcaoprg  10607  iseqf1olemab  10613  iseqf1olemnanb  10614  seqf1oglem1  10630  expnegzap  10684  nn0ltexp2  10820  hashen  10895  hashunlem  10915  hashprg  10919  leisorel  10948  zfz1isolemiso  10950  seq3coll  10953  caucvgrelemrec  11163  resqrexlemex  11209  minmax  11414  xrminmax  11449  fsum2dlemstep  11618  fisumcom2  11622  zproddc  11763  fprod2dlemstep  11806  fprodcom2fi  11810  bezoutlemmain  12192  sqgcd  12223  pcpremul  12489  pceulem  12490  pceu  12491  pczpre  12493  pcdiv  12498  pcqmul  12499  pcqdiv  12503  pcexp  12505  pcdvdsb  12516  pcneg  12521  pcdvdstr  12523  pcgcd1  12524  pc2dvds  12526  pcz  12528  pcaddlem  12535  pcadd  12536  qexpz  12548  expnprm  12549  infpnlem2  12556  f1ocpbllem  13014  f1ovscpbl  13016  sgrppropd  13117  mndpropd  13144  grpsubpropd2  13309  f1ghm0to0  13480  ablnnncan  13531  rngpropd  13589  ringpropd  13672  lmodprop2d  13982  lsspropdg  14065  neiint  14489  restbasg  14512  iscnp4  14562  cnconst2  14577  cnpdis  14586  neitx  14612  upxp  14616  hmeoimaf1o  14658  blssexps  14773  blssex  14774  ssblex  14775  bdmopn  14848  xmettx  14854  metcnp3  14855  tgioo  14898  tgqioo  14899  dvmptfsum  15069  elply2  15079  sin0pilem2  15126  logbgcd1irr  15311  perfect  15345  lgsval  15353  lgsfcl2  15355  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  1dom1el  15745  pwle2  15753