Theorem syl22anc 1279

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 1276	1 |- ( ph -> et )

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:  f1oprg  5685  tfrexlem  6605  th3qlem1  6911  en2prd  7106  enpr2d  7111  ssenen  7152  phplem4dom  7163  phplem4on  7169  fiunsnnn  7185  findcard2sd  7196  unsnfi  7226  sbthlemi9  7282  fsuppcorn  7301  endjusym  7437  endjudisj  7567  djuen  7568  ltanqg  7768  ltmnqg  7769  ltnnnq  7791  addcmpblnq0  7811  addlocprlemeqgt  7900  distrlem1prl  7950  distrlem1pru  7951  distrlem4prl  7952  distrlem4pru  7953  addcanprleml  7982  recexprlem1ssl  8001  caucvgprlemloc  8043  caucvgprprlemloccalc  8052  mulcmpblnr  8109  ltasrg  8138  recexgt0sr  8141  mulextsr1lem  8148  mulextsr1  8149  srpospr  8151  prsrlt  8155  ltpsrprg  8171  mappsrprg  8172  pitonnlem1p1  8214  recidpirq  8226  axpre-ltadd  8254  mulgt0d  8451  mul4d  8483  add4d  8497  add42d  8498  subcan  8583  addsub4d  8686  subadd4d  8687  sub4d  8688  2addsubd  8689  addsubeq4d  8690  muladdd  8745  mulsubd  8746  addgegt0d  8849  addgtge0d  8850  addge0d  8852  le2addd  8894  le2subd  8895  ltleaddd  8896  leltaddd  8897  lt2subd  8899  apreap  8918  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  mulap0r  8946  mulge0d  8952  mulap0d  8989  divdivdivap  9046  divcanap5  9047  divap0d  9139  recdivapd  9140  recdivap2d  9141  divcanap6d  9142  ddcanapd  9143  rec11apd  9144  divmuldivapd  9165  divmuleqapd  9166  subrecapd  9174  prodgt0  9185  lt2msq  9219  ledivdiv  9223  lediv12a  9227  recreclt  9233  divgt0d  9268  mulgt1d  9269  lemulge11d  9270  lemulge12d  9271  ltmul12ad  9274  lemul12ad  9275  lemul12bd  9276  nndivtr  9349  qreccl  10052  ledivdivd  10134  lediv12ad  10168  lt2mul2divd  10177  xlt2add  10293  xleaddadd  10300  iccss2  10357  iccssico2  10360  lincmb01cmp  10416  iccf1o  10418  fzrev2i  10504  qtri3or  10686  elicore  10712  2tnp1ge0ge0  10751  modqid  10801  q0mod  10807  q1mod  10808  modqabs  10809  modqadd1  10813  mulqaddmodid  10816  mulp1mod1  10817  modqmuladd  10818  modqmuladdnn0  10820  qnegmod  10821  m1modnnsub1  10822  addmodid  10824  modqm1p1mod0  10827  modqltm1p1mod  10828  modqmul1  10829  q2submod  10837  modifeq2int  10838  modaddmodup  10839  modaddmodlo  10840  modqaddmulmod  10843  modqsubdir  10845  modqeqmodmin  10846  modsumfzodifsn  10848  addmodlteq  10850  frecfzennn  10878  ser3mono  10939  expcl2lemap  11003  mulexpzap  11031  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  ltexp2a  11043  leexp2a  11044  sqdivap  11055  qsqeqor  11102  expnbnd  11116  expsubapd  11137  lt2sqd  11157  le2sqd  11158  sq11d  11159  apexp1  11172  bcp1nk  11216  hashunlem  11260  hashf1lem1  11301  zfz1isolem1  11308  hashtpgim  11313  sq01  11676  cjap  11688  cnreim  11760  resqrexlem1arp  11787  resqrexlemp1rp  11788  resqrexlemglsq  11804  abs00ap  11844  absext  11845  absexpzap  11863  absrele  11866  sqrtmuld  11952  sqrtsq2d  11953  sqrtled  11954  sqrtltd  11955  sqr11d  11956  abs3lemd  11984  minmax  12014  xrmaxiflemlub  12033  xrltmaxsup  12042  xrminmax  12050  xrbdtri  12061  climuni  12078  2clim  12086  addcn2  12095  mulcn2  12097  fsum3  12173  mptfzshft  12228  fsumrev  12229  fisum0diag2  12233  modfsummodlemstep  12243  binomlem  12269  mertenslemi1  12321  fprodrev  12405  efcllemp  12444  p1modz1  12580  dvds1  12639  dvdsext  12641  mulmoddvds  12649  oexpneg  12663  evennn02n  12668  evennn2n  12669  bitsinv1  12748  bezoutlemmo  12802  mulgcd  12812  dvdssqlem  12826  rpmulgcd2  12892  isprm6  12945  sqrt2irraplemnn  12978  sqrt2irrap  12979  sqrtrirr  13008  crth  13025  eulerthlemh  13032  prmdiveq  13037  powm2modprm  13054  modprm0  13056  pythagtriplem2  13068  pythagtriplem11  13076  pythagtriplem13  13078  pythagtrip  13085  pcid  13126  pcgcd1  13130  pcprmpw2  13135  dvdsprmpweqle  13139  pcaddlem  13141  pcadd  13142  fldivp1  13150  4sqlem12  13204  4sqlem14  13206  4sqlem15  13207  4sqlem16  13208  ballotfilemsima  13311  ballotfilemfrceq  13324  unennn  13340  ennnfonelemg  13346  ennnfonelemhf1o  13356  inffinp1  13372  isstructr  13419  setscomd  13445  imasbas  13681  imasplusg  13682  imasmulr  13683  subm0  13842  gzsumshift  14233  gsump1  14241  lssvancl1  14788  lssvnegcl  14797  lspprvacl  14834  lspsneli  14836  lspsn  14837  znf1o  15070  ntrin  15316  topssnei  15354  restbasg  15360  cnntri  15416  txcn  15467  txlm  15471  cnmpt2res  15489  psmetlecl  15526  xmetlecl  15559  bldisj  15593  bdmet  15694  bdbl  15695  bdmopn  15696  xmetxp  15699  metcnp  15704  tgioo  15746  cncfmet  15784  dedekindeulemlub  15812  suplociccreex  15816  ellimc3apf  15852  limcimolemlt  15856  limccnp2cntop  15869  dvfvalap  15873  dvidsslem  15885  dvmulxxbr  15894  dvaddxx  15895  dvmulxx  15896  dviaddf  15897  dvimulf  15898  dvcoapbr  15899  dvmptclx  15910  cxplt3  16117  cxpltd  16125  cxpled  16126  cxplt3d  16132  cxple3d  16133  logbrec  16157  logbgcd1irraplemap  16166  zprmlogbaplem1  16176  log2tlbndlog2  16181  birthdaylem3  16188  pellexlem1  16190  pellexlem2  16191  wilthlem1  16193  ppiqsval  16201  chtqwordi  16224  ppiqwordi  16229  mpodvdsmulf1o  16245  ppiqub  16254  bclbnd  16268  bposlem7  16278  lgslem1  16285  lgslem3  16287  lgsdirprm  16319  gausslemma2dlem1f1o  16345  gausslemma2dlem6  16352  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem4  16358  lgseisen  16359  lgsquadlem1  16362  lgsquad2lem1  16366  lgsquad3  16369  m1lgs  16370  2lgslem1a1  16371  2sqlem7  16406  usgredg2v  16631  vtxd0nedgbfi  16706  clwwlknonex2  16846