Theorem syl22anc 1272

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
sylXanc.1	|- ( ph -> ps )
sylXanc.2	|- ( ph -> ch )
sylXanc.3	|- ( ph -> th )
sylXanc.4	|- ( ph -> ta )
syl22anc.5	|- ( ( ( ps /\ ch ) /\ ( th /\ ta ) ) -> et )

Assertion

Ref	Expression
syl22anc	|- ( ph -> et )

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 306	. 2 |- ( ph -> ( ps /\ ch ) )
4		sylXanc.3	. 2 |- ( ph -> th )
5		sylXanc.4	. 2 |- ( ph -> ta )
6		syl22anc.5	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) ) -> et )
7	3, 4, 5, 6	syl12anc 1269	1 |- ( ph -> et )

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:  f1oprg  5616  tfrexlem  6478  th3qlem1  6782  en2prd  6968  enpr2d  6970  ssenen  7008  phplem4dom  7019  phplem4on  7025  fiunsnnn  7039  findcard2sd  7050  unsnfi  7077  sbthlemi9  7128  endjusym  7259  endjudisj  7388  djuen  7389  ltanqg  7583  ltmnqg  7584  ltnnnq  7606  addcmpblnq0  7626  addlocprlemeqgt  7715  distrlem1prl  7765  distrlem1pru  7766  distrlem4prl  7767  distrlem4pru  7768  addcanprleml  7797  recexprlem1ssl  7816  caucvgprlemloc  7858  caucvgprprlemloccalc  7867  mulcmpblnr  7924  ltasrg  7953  recexgt0sr  7956  mulextsr1lem  7963  mulextsr1  7964  srpospr  7966  prsrlt  7970  ltpsrprg  7986  mappsrprg  7987  pitonnlem1p1  8029  recidpirq  8041  axpre-ltadd  8069  mulgt0d  8265  mul4d  8297  add4d  8311  add42d  8312  subcan  8397  addsub4d  8500  subadd4d  8501  sub4d  8502  2addsubd  8503  addsubeq4d  8504  muladdd  8558  mulsubd  8559  addgegt0d  8662  addgtge0d  8663  addge0d  8665  le2addd  8706  le2subd  8707  ltleaddd  8708  leltaddd  8709  lt2subd  8711  apreap  8730  apsym  8749  apcotr  8750  apadd1  8751  apneg  8754  mulext1  8755  mulap0r  8758  mulge0d  8764  mulap0d  8801  divdivdivap  8856  divcanap5  8857  divap0d  8949  recdivapd  8950  recdivap2d  8951  divcanap6d  8952  ddcanapd  8953  rec11apd  8954  divmuldivapd  8975  divmuleqapd  8976  subrecapd  8984  prodgt0  8995  lt2msq  9029  ledivdiv  9033  lediv12a  9037  recreclt  9043  divgt0d  9078  mulgt1d  9079  lemulge11d  9080  lemulge12d  9081  ltmul12ad  9084  lemul12ad  9085  lemul12bd  9086  nndivtr  9148  qreccl  9833  ledivdivd  9914  lediv12ad  9948  lt2mul2divd  9957  xlt2add  10072  xleaddadd  10079  iccss2  10136  iccssico2  10139  lincmb01cmp  10195  iccf1o  10196  fzrev2i  10278  qtri3or  10455  elicore  10481  2tnp1ge0ge0  10516  modqid  10566  q0mod  10572  q1mod  10573  modqabs  10574  modqadd1  10578  mulqaddmodid  10581  mulp1mod1  10582  modqmuladd  10583  modqmuladdnn0  10585  qnegmod  10586  m1modnnsub1  10587  addmodid  10589  modqm1p1mod0  10592  modqltm1p1mod  10593  modqmul1  10594  q2submod  10602  modifeq2int  10603  modaddmodup  10604  modaddmodlo  10605  modqaddmulmod  10608  modqsubdir  10610  modqeqmodmin  10611  modsumfzodifsn  10613  addmodlteq  10615  frecfzennn  10643  ser3mono  10704  expcl2lemap  10768  mulexpzap  10796  expaddzaplem  10799  expaddzap  10800  expmulzap  10802  ltexp2a  10808  leexp2a  10809  sqdivap  10820  qsqeqor  10867  expnbnd  10880  expsubapd  10901  lt2sqd  10921  le2sqd  10922  sq11d  10923  apexp1  10935  bcp1nk  10979  hashunlem  11021  zfz1isolem1  11057  cjap  11412  cnreim  11484  resqrexlem1arp  11511  resqrexlemp1rp  11512  resqrexlemglsq  11528  abs00ap  11568  absext  11569  absexpzap  11586  absrele  11589  sqrtmuld  11675  sqrtsq2d  11676  sqrtled  11677  sqrtltd  11678  sqr11d  11679  abs3lemd  11707  minmax  11736  xrmaxiflemlub  11754  xrltmaxsup  11763  xrminmax  11771  xrbdtri  11782  climuni  11799  2clim  11807  addcn2  11816  mulcn2  11818  fsum3  11893  mptfzshft  11948  fsumrev  11949  fisum0diag2  11953  modfsummodlemstep  11963  binomlem  11989  mertenslemi1  12041  fprodrev  12125  efcllemp  12164  p1modz1  12300  dvds1  12359  dvdsext  12361  mulmoddvds  12369  oexpneg  12383  evennn02n  12388  evennn2n  12389  bitsinv1  12468  bezoutlemmo  12522  mulgcd  12532  dvdssqlem  12546  rpmulgcd2  12612  isprm6  12664  sqrt2irraplemnn  12696  sqrt2irrap  12697  crth  12741  eulerthlemh  12748  prmdiveq  12753  powm2modprm  12770  modprm0  12772  pythagtriplem2  12784  pythagtriplem11  12792  pythagtriplem13  12794  pythagtrip  12801  pcid  12842  pcgcd1  12846  pcprmpw2  12851  dvdsprmpweqle  12855  pcaddlem  12857  pcadd  12858  fldivp1  12866  4sqlem12  12920  4sqlem14  12922  4sqlem15  12923  4sqlem16  12924  unennn  12963  ennnfonelemg  12969  ennnfonelemhf1o  12979  inffinp1  12995  isstructr  13042  setscomd  13068  imasbas  13335  imasplusg  13336  imasmulr  13337  subm0  13510  lssvancl1  14325  lssvnegcl  14334  lspprvacl  14371  lspsneli  14373  lspsn  14374  znf1o  14609  ntrin  14792  topssnei  14830  restbasg  14836  cnntri  14892  txcn  14943  txlm  14947  cnmpt2res  14965  psmetlecl  15002  xmetlecl  15035  bldisj  15069  bdmet  15170  bdbl  15171  bdmopn  15172  xmetxp  15175  metcnp  15180  tgioo  15222  cncfmet  15260  dedekindeulemlub  15288  suplociccreex  15292  ellimc3apf  15328  limcimolemlt  15332  limccnp2cntop  15345  dvfvalap  15349  dvidsslem  15361  dvmulxxbr  15370  dvaddxx  15371  dvmulxx  15372  dviaddf  15373  dvimulf  15374  dvcoapbr  15375  dvmptclx  15386  cxplt3  15588  cxpltd  15596  cxpled  15597  cxplt3d  15603  cxple3d  15604  logbrec  15628  logbgcd1irraplemap  15637  wilthlem1  15648  mpodvdsmulf1o  15658  lgslem1  15673  lgslem3  15675  lgsdirprm  15707  gausslemma2dlem1f1o  15733  gausslemma2dlem6  15740  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem4  15746  lgseisen  15747  lgsquadlem1  15750  lgsquad2lem1  15754  lgsquad3  15757  m1lgs  15758  2lgslem1a1  15759  2sqlem7  15794  usgredg2v  16016