Theorem syl22anc 1239

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 1236	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  5506  tfrexlem  6335  th3qlem1  6637  enpr2d  6817  ssenen  6851  phplem4dom  6862  phplem4on  6867  fiunsnnn  6881  findcard2sd  6892  unsnfi  6918  sbthlemi9  6964  endjusym  7095  endjudisj  7209  djuen  7210  ltanqg  7399  ltmnqg  7400  ltnnnq  7422  addcmpblnq0  7442  addlocprlemeqgt  7531  distrlem1prl  7581  distrlem1pru  7582  distrlem4prl  7583  distrlem4pru  7584  addcanprleml  7613  recexprlem1ssl  7632  caucvgprlemloc  7674  caucvgprprlemloccalc  7683  mulcmpblnr  7740  ltasrg  7769  recexgt0sr  7772  mulextsr1lem  7779  mulextsr1  7780  srpospr  7782  prsrlt  7786  ltpsrprg  7802  mappsrprg  7803  pitonnlem1p1  7845  recidpirq  7857  axpre-ltadd  7885  mulgt0d  8080  mul4d  8112  add4d  8126  add42d  8127  subcan  8212  addsub4d  8315  subadd4d  8316  sub4d  8317  2addsubd  8318  addsubeq4d  8319  muladdd  8373  mulsubd  8374  addgegt0d  8476  addgtge0d  8477  addge0d  8479  le2addd  8520  le2subd  8521  ltleaddd  8522  leltaddd  8523  lt2subd  8525  apreap  8544  apsym  8563  apcotr  8564  apadd1  8565  apneg  8568  mulext1  8569  mulap0r  8572  mulge0d  8578  mulap0d  8615  divdivdivap  8670  divcanap5  8671  divap0d  8763  recdivapd  8764  recdivap2d  8765  divcanap6d  8766  ddcanapd  8767  rec11apd  8768  divmuldivapd  8789  divmuleqapd  8790  subrecapd  8798  prodgt0  8809  lt2msq  8843  ledivdiv  8847  lediv12a  8851  recreclt  8857  divgt0d  8892  mulgt1d  8893  lemulge11d  8894  lemulge12d  8895  ltmul12ad  8898  lemul12ad  8899  lemul12bd  8900  nndivtr  8961  qreccl  9642  ledivdivd  9722  lediv12ad  9756  lt2mul2divd  9765  xlt2add  9880  xleaddadd  9887  iccss2  9944  iccssico2  9947  lincmb01cmp  10003  iccf1o  10004  fzrev2i  10086  qtri3or  10243  elicore  10267  2tnp1ge0ge0  10301  modqid  10349  q0mod  10355  q1mod  10356  modqabs  10357  modqadd1  10361  mulqaddmodid  10364  mulp1mod1  10365  modqmuladd  10366  modqmuladdnn0  10368  qnegmod  10369  m1modnnsub1  10370  addmodid  10372  modqm1p1mod0  10375  modqltm1p1mod  10376  modqmul1  10377  q2submod  10385  modifeq2int  10386  modaddmodup  10387  modaddmodlo  10388  modqaddmulmod  10391  modqsubdir  10393  modqeqmodmin  10394  modsumfzodifsn  10396  addmodlteq  10398  frecfzennn  10426  ser3mono  10478  expcl2lemap  10532  mulexpzap  10560  expaddzaplem  10563  expaddzap  10564  expmulzap  10566  ltexp2a  10572  leexp2a  10573  sqdivap  10584  qsqeqor  10631  expnbnd  10644  expsubapd  10665  lt2sqd  10685  le2sqd  10686  sq11d  10687  apexp1  10698  bcp1nk  10742  hashunlem  10784  zfz1isolem1  10820  cjap  10915  cnreim  10987  resqrexlem1arp  11014  resqrexlemp1rp  11015  resqrexlemglsq  11031  abs00ap  11071  absext  11072  absexpzap  11089  absrele  11092  sqrtmuld  11178  sqrtsq2d  11179  sqrtled  11180  sqrtltd  11181  sqr11d  11182  abs3lemd  11210  minmax  11238  xrmaxiflemlub  11256  xrltmaxsup  11265  xrminmax  11273  xrbdtri  11284  climuni  11301  2clim  11309  addcn2  11318  mulcn2  11320  fsum3  11395  mptfzshft  11450  fsumrev  11451  fisum0diag2  11455  modfsummodlemstep  11465  binomlem  11491  mertenslemi1  11543  fprodrev  11627  efcllemp  11666  p1modz1  11801  dvds1  11859  dvdsext  11861  mulmoddvds  11869  oexpneg  11882  evennn02n  11887  evennn2n  11888  bezoutlemmo  12007  mulgcd  12017  dvdssqlem  12031  rpmulgcd2  12095  isprm6  12147  sqrt2irraplemnn  12179  sqrt2irrap  12180  crth  12224  eulerthlemh  12231  prmdiveq  12236  powm2modprm  12252  modprm0  12254  pythagtriplem2  12266  pythagtriplem11  12274  pythagtriplem13  12276  pythagtrip  12283  pcid  12323  pcgcd1  12327  pcprmpw2  12332  dvdsprmpweqle  12336  pcaddlem  12338  pcadd  12339  fldivp1  12346  unennn  12398  ennnfonelemg  12404  ennnfonelemhf1o  12414  inffinp1  12430  isstructr  12477  setscomd  12503  imasbas  12728  imasplusg  12729  imasmulr  12730  ntrin  13627  topssnei  13665  restbasg  13671  cnntri  13727  txcn  13778  txlm  13782  cnmpt2res  13800  psmetlecl  13837  xmetlecl  13870  bldisj  13904  bdmet  14005  bdbl  14006  bdmopn  14007  xmetxp  14010  metcnp  14015  tgioo  14049  cncfmet  14082  dedekindeulemlub  14101  suplociccreex  14105  ellimc3apf  14132  limcimolemlt  14136  limccnp2cntop  14149  dvfvalap  14153  dvmulxxbr  14169  dvaddxx  14170  dvmulxx  14171  dviaddf  14172  dvimulf  14173  dvcoapbr  14174  dvmptclx  14183  cxplt3  14343  cxpltd  14351  cxpled  14352  cxplt3d  14357  cxple3d  14358  logbrec  14381  logbgcd1irraplemap  14390  lgslem1  14404  lgslem3  14406  lgsdirprm  14438  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2sqlem7  14471