Theorem syl12anc 1271

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  1274  cocan1  5933  fliftfun  5942  isopolem  5968  f1oiso2  5973  caovcld  6181  caovcomd  6184  tfrlemisucaccv  6496  tfr1onlemsucaccv  6512  tfr1onlembxssdm  6514  tfrcllemsucaccv  6525  tfrcllembxssdm  6527  1dom1el  6998  fidceq  7061  findcard2d  7085  diffifi  7088  tridc  7094  en2eqpr  7104  sbthlemi9  7169  supisolem  7212  ordiso2  7239  difinfsnlem  7303  difinfsn  7304  pr2cv1  7405  prarloclemup  7720  prarloc  7728  nqprl  7776  nqpru  7777  ltaddpr  7822  aptiprlemu  7865  archpr  7868  cauappcvgprlem2  7885  caucvgprlem2  7905  caucvgprprlem2  7935  suplocexprlemlub  7949  suplocexpr  7950  recexgt0sr  7998  archsr  8007  axpre-suploclemres  8126  conjmulap  8914  lerec2  9074  ledivp1  9088  cju  9146  nn2ge  9181  gtndiv  9580  supinfneg  9834  infsupneg  9835  z2ge  10066  iccssioo2  10186  fzrev3  10327  elfz1b  10330  zsupcllemstep  10495  zsupssdc  10504  exbtwnzlemstep  10513  exbtwnzlemex  10515  rebtwn2zlemstep  10518  rebtwn2z  10520  qbtwnre  10522  flqdiv  10589  frec2uzled  10697  seq3caopr  10763  seqcaoprg  10764  iseqf1olemab  10770  iseqf1olemnanb  10771  seqf1oglem1  10787  expnegzap  10841  nn0ltexp2  10977  hashen  11052  hashunlem  11073  hashprg  11078  leisorel  11107  zfz1isolemiso  11109  seq3coll  11112  swrdccat3b  11330  caucvgrelemrec  11562  resqrexlemex  11608  minmax  11813  xrminmax  11848  fsum2dlemstep  12018  fisumcom2  12022  zproddc  12163  fprod2dlemstep  12206  fprodcom2fi  12210  bezoutlemmain  12592  sqgcd  12623  pcpremul  12889  pceulem  12890  pceu  12891  pczpre  12893  pcdiv  12898  pcqmul  12899  pcqdiv  12903  pcexp  12905  pcdvdsb  12916  pcneg  12921  pcdvdstr  12923  pcgcd1  12924  pc2dvds  12926  pcz  12928  pcaddlem  12935  pcadd  12936  qexpz  12948  expnprm  12949  infpnlem2  12956  f1ocpbllem  13416  f1ovscpbl  13418  sgrppropd  13519  mndpropd  13546  grpsubpropd2  13711  f1ghm0to0  13882  ablnnncan  13933  rngpropd  13992  ringpropd  14075  lmodprop2d  14386  lsspropdg  14469  neiint  14898  restbasg  14921  iscnp4  14971  cnconst2  14986  cnpdis  14995  neitx  15021  upxp  15025  hmeoimaf1o  15067  blssexps  15182  blssex  15183  ssblex  15184  bdmopn  15257  xmettx  15263  metcnp3  15264  tgioo  15307  tgqioo  15308  dvmptfsum  15478  elply2  15488  sin0pilem2  15535  logbgcd1irr  15720  perfect  15754  lgsval  15762  lgsfcl2  15764  lgsdir  15793  lgsdilem2  15794  lgsdi  15795  lgsne0  15796  clwwlknonex2e  16320  pwle2  16659  qdiff  16720