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  5993  fliftfun  6002  isopolem  6028  f1oiso2  6033  caovcld  6243  caovcomd  6246  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  1dom1el  7107  fidceq  7171  findcard2d  7195  diffifi  7198  tridc  7204  en2eqpr  7214  sbthlemi9  7282  supisolem  7348  ordiso2  7375  difinfsnlem  7439  difinfsn  7440  pr2cv1  7541  prarloclemup  7862  prarloc  7870  nqprl  7918  nqpru  7919  ltaddpr  7964  aptiprlemu  8007  archpr  8010  cauappcvgprlem2  8027  caucvgprlem2  8047  caucvgprprlem2  8077  suplocexprlemlub  8091  suplocexpr  8092  recexgt0sr  8140  archsr  8149  axpre-suploclemres  8268  conjmulap  9060  lerec2  9220  ledivp1  9234  cju  9292  nn2ge  9338  gtndiv  9743  supinfneg  9997  infsupneg  9998  z2ge  10230  iccssioo2  10350  fzrev3  10496  elfz1b  10499  zsupcllemstep  10664  zsupssdc  10675  exbtwnzlemstep  10684  exbtwnzlemex  10686  rebtwn2zlemstep  10689  rebtwn2z  10691  qbtwnre  10693  flqdiv  10760  frec2uzled  10868  seq3caopr  10934  seqcaoprg  10935  iseqf1olemab  10941  iseqf1olemnanb  10942  seqf1oglem1  10958  expnegzap  11012  nn0ltexp2  11149  hashen  11225  hashunlem  11246  hashprg  11251  hashfibclem  11284  hashf1lem2  11288  leisorel  11291  zfz1isolemiso  11293  seq3coll  11296  swrdccat3b  11514  caucvgrelemrec  11747  resqrexlemex  11793  minmax  11998  xrminmax  12033  fsum2dlemstep  12203  fisumcom2  12207  zproddc  12348  fprod2dlemstep  12391  fprodcom2fi  12395  bezoutlemmain  12777  sqgcd  12808  pcpremul  13074  pceulem  13075  pceu  13076  pczpre  13078  pcdiv  13083  pcqmul  13084  pcqdiv  13088  pcexp  13090  pcdvdsb  13101  pcneg  13106  pcdvdstr  13108  pcgcd1  13109  pc2dvds  13111  pcz  13113  pcaddlem  13120  pcadd  13121  qexpz  13133  expnprm  13134  infpnlem2  13141  ballotfilemfc0  13234  ballotfilemfcc  13235  f1ocpbllem  13633  f1ovscpbl  13635  sgrppropd  13730  mndpropd  13755  grpsubpropd2  13912  f1ghm0to0  14077  ablnnncan  14129  rngpropd  14256  ringpropd  14345  lmodprop2d  14687  lsspropdg  14770  assapropd  15016  neiint  15248  restbasg  15271  iscnp4  15321  cnconst2  15336  cnpdis  15345  neitx  15371  upxp  15375  hmeoimaf1o  15417  blssexps  15532  blssex  15533  ssblex  15534  bdmopn  15607  xmettx  15613  metcnp3  15614  tgioo  15657  tgqioo  15658  dvmptfsum  15828  elply2  15838  sin0pilem2  15886  logbgcd1irr  16075  perfect  16121  lgsval  16135  lgsfcl2  16137  lgsdir  16166  lgsdilem2  16167  lgsdi  16168  lgsne0  16169  clwwlknonex2e  16693  pwle2  17040  qdiff  17110