Theorem syl12anc 1269

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  1272  cocan1  5923  fliftfun  5932  isopolem  5958  f1oiso2  5963  caovcld  6171  caovcomd  6174  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  1dom1el  6988  fidceq  7051  findcard2d  7075  diffifi  7078  tridc  7084  en2eqpr  7094  sbthlemi9  7158  supisolem  7201  ordiso2  7228  difinfsnlem  7292  difinfsn  7293  pr2cv1  7394  prarloclemup  7708  prarloc  7716  nqprl  7764  nqpru  7765  ltaddpr  7810  aptiprlemu  7853  archpr  7856  cauappcvgprlem2  7873  caucvgprlem2  7893  caucvgprprlem2  7923  suplocexprlemlub  7937  suplocexpr  7938  recexgt0sr  7986  archsr  7995  axpre-suploclemres  8114  conjmulap  8902  lerec2  9062  ledivp1  9076  cju  9134  nn2ge  9169  gtndiv  9568  supinfneg  9822  infsupneg  9823  z2ge  10054  iccssioo2  10174  fzrev3  10315  elfz1b  10318  zsupcllemstep  10482  zsupssdc  10491  exbtwnzlemstep  10500  exbtwnzlemex  10502  rebtwn2zlemstep  10505  rebtwn2z  10507  qbtwnre  10509  flqdiv  10576  frec2uzled  10684  seq3caopr  10750  seqcaoprg  10751  iseqf1olemab  10757  iseqf1olemnanb  10758  seqf1oglem1  10774  expnegzap  10828  nn0ltexp2  10964  hashen  11039  hashunlem  11060  hashprg  11065  leisorel  11094  zfz1isolemiso  11096  seq3coll  11099  swrdccat3b  11314  caucvgrelemrec  11533  resqrexlemex  11579  minmax  11784  xrminmax  11819  fsum2dlemstep  11988  fisumcom2  11992  zproddc  12133  fprod2dlemstep  12176  fprodcom2fi  12180  bezoutlemmain  12562  sqgcd  12593  pcpremul  12859  pceulem  12860  pceu  12861  pczpre  12863  pcdiv  12868  pcqmul  12869  pcqdiv  12873  pcexp  12875  pcdvdsb  12886  pcneg  12891  pcdvdstr  12893  pcgcd1  12894  pc2dvds  12896  pcz  12898  pcaddlem  12905  pcadd  12906  qexpz  12918  expnprm  12919  infpnlem2  12926  f1ocpbllem  13386  f1ovscpbl  13388  sgrppropd  13489  mndpropd  13516  grpsubpropd2  13681  f1ghm0to0  13852  ablnnncan  13903  rngpropd  13961  ringpropd  14044  lmodprop2d  14355  lsspropdg  14438  neiint  14862  restbasg  14885  iscnp4  14935  cnconst2  14950  cnpdis  14959  neitx  14985  upxp  14989  hmeoimaf1o  15031  blssexps  15146  blssex  15147  ssblex  15148  bdmopn  15221  xmettx  15227  metcnp3  15228  tgioo  15271  tgqioo  15272  dvmptfsum  15442  elply2  15452  sin0pilem2  15499  logbgcd1irr  15684  perfect  15718  lgsval  15726  lgsfcl2  15728  lgsdir  15757  lgsdilem2  15758  lgsdi  15759  lgsne0  15760  clwwlknonex2e  16249  pwle2  16549