Theorem syl22anc 1250

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 1247	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  5565  tfrexlem  6419  th3qlem1  6723  en2prd  6908  enpr2d  6910  ssenen  6947  phplem4dom  6958  phplem4on  6963  fiunsnnn  6977  findcard2sd  6988  unsnfi  7015  sbthlemi9  7066  endjusym  7197  endjudisj  7321  djuen  7322  ltanqg  7512  ltmnqg  7513  ltnnnq  7535  addcmpblnq0  7555  addlocprlemeqgt  7644  distrlem1prl  7694  distrlem1pru  7695  distrlem4prl  7696  distrlem4pru  7697  addcanprleml  7726  recexprlem1ssl  7745  caucvgprlemloc  7787  caucvgprprlemloccalc  7796  mulcmpblnr  7853  ltasrg  7882  recexgt0sr  7885  mulextsr1lem  7892  mulextsr1  7893  srpospr  7895  prsrlt  7899  ltpsrprg  7915  mappsrprg  7916  pitonnlem1p1  7958  recidpirq  7970  axpre-ltadd  7998  mulgt0d  8194  mul4d  8226  add4d  8240  add42d  8241  subcan  8326  addsub4d  8429  subadd4d  8430  sub4d  8431  2addsubd  8432  addsubeq4d  8433  muladdd  8487  mulsubd  8488  addgegt0d  8591  addgtge0d  8592  addge0d  8594  le2addd  8635  le2subd  8636  ltleaddd  8637  leltaddd  8638  lt2subd  8640  apreap  8659  apsym  8678  apcotr  8679  apadd1  8680  apneg  8683  mulext1  8684  mulap0r  8687  mulge0d  8693  mulap0d  8730  divdivdivap  8785  divcanap5  8786  divap0d  8878  recdivapd  8879  recdivap2d  8880  divcanap6d  8881  ddcanapd  8882  rec11apd  8883  divmuldivapd  8904  divmuleqapd  8905  subrecapd  8913  prodgt0  8924  lt2msq  8958  ledivdiv  8962  lediv12a  8966  recreclt  8972  divgt0d  9007  mulgt1d  9008  lemulge11d  9009  lemulge12d  9010  ltmul12ad  9013  lemul12ad  9014  lemul12bd  9015  nndivtr  9077  qreccl  9762  ledivdivd  9843  lediv12ad  9877  lt2mul2divd  9886  xlt2add  10001  xleaddadd  10008  iccss2  10065  iccssico2  10068  lincmb01cmp  10124  iccf1o  10125  fzrev2i  10207  qtri3or  10381  elicore  10407  2tnp1ge0ge0  10442  modqid  10492  q0mod  10498  q1mod  10499  modqabs  10500  modqadd1  10504  mulqaddmodid  10507  mulp1mod1  10508  modqmuladd  10509  modqmuladdnn0  10511  qnegmod  10512  m1modnnsub1  10513  addmodid  10515  modqm1p1mod0  10518  modqltm1p1mod  10519  modqmul1  10520  q2submod  10528  modifeq2int  10529  modaddmodup  10530  modaddmodlo  10531  modqaddmulmod  10534  modqsubdir  10536  modqeqmodmin  10537  modsumfzodifsn  10539  addmodlteq  10541  frecfzennn  10569  ser3mono  10630  expcl2lemap  10694  mulexpzap  10722  expaddzaplem  10725  expaddzap  10726  expmulzap  10728  ltexp2a  10734  leexp2a  10735  sqdivap  10746  qsqeqor  10793  expnbnd  10806  expsubapd  10827  lt2sqd  10847  le2sqd  10848  sq11d  10849  apexp1  10861  bcp1nk  10905  hashunlem  10947  zfz1isolem1  10983  cjap  11188  cnreim  11260  resqrexlem1arp  11287  resqrexlemp1rp  11288  resqrexlemglsq  11304  abs00ap  11344  absext  11345  absexpzap  11362  absrele  11365  sqrtmuld  11451  sqrtsq2d  11452  sqrtled  11453  sqrtltd  11454  sqr11d  11455  abs3lemd  11483  minmax  11512  xrmaxiflemlub  11530  xrltmaxsup  11539  xrminmax  11547  xrbdtri  11558  climuni  11575  2clim  11583  addcn2  11592  mulcn2  11594  fsum3  11669  mptfzshft  11724  fsumrev  11725  fisum0diag2  11729  modfsummodlemstep  11739  binomlem  11765  mertenslemi1  11817  fprodrev  11901  efcllemp  11940  p1modz1  12076  dvds1  12135  dvdsext  12137  mulmoddvds  12145  oexpneg  12159  evennn02n  12164  evennn2n  12165  bitsinv1  12244  bezoutlemmo  12298  mulgcd  12308  dvdssqlem  12322  rpmulgcd2  12388  isprm6  12440  sqrt2irraplemnn  12472  sqrt2irrap  12473  crth  12517  eulerthlemh  12524  prmdiveq  12529  powm2modprm  12546  modprm0  12548  pythagtriplem2  12560  pythagtriplem11  12568  pythagtriplem13  12570  pythagtrip  12577  pcid  12618  pcgcd1  12622  pcprmpw2  12627  dvdsprmpweqle  12631  pcaddlem  12633  pcadd  12634  fldivp1  12642  4sqlem12  12696  4sqlem14  12698  4sqlem15  12699  4sqlem16  12700  unennn  12739  ennnfonelemg  12745  ennnfonelemhf1o  12755  inffinp1  12771  isstructr  12818  setscomd  12844  imasbas  13110  imasplusg  13111  imasmulr  13112  subm0  13285  lssvancl1  14100  lssvnegcl  14109  lspprvacl  14146  lspsneli  14148  lspsn  14149  znf1o  14384  ntrin  14567  topssnei  14605  restbasg  14611  cnntri  14667  txcn  14718  txlm  14722  cnmpt2res  14740  psmetlecl  14777  xmetlecl  14810  bldisj  14844  bdmet  14945  bdbl  14946  bdmopn  14947  xmetxp  14950  metcnp  14955  tgioo  14997  cncfmet  15035  dedekindeulemlub  15063  suplociccreex  15067  ellimc3apf  15103  limcimolemlt  15107  limccnp2cntop  15120  dvfvalap  15124  dvidsslem  15136  dvmulxxbr  15145  dvaddxx  15146  dvmulxx  15147  dviaddf  15148  dvimulf  15149  dvcoapbr  15150  dvmptclx  15161  cxplt3  15363  cxpltd  15371  cxpled  15372  cxplt3d  15378  cxple3d  15379  logbrec  15403  logbgcd1irraplemap  15412  wilthlem1  15423  mpodvdsmulf1o  15433  lgslem1  15448  lgslem3  15450  lgsdirprm  15482  gausslemma2dlem1f1o  15508  gausslemma2dlem6  15515  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem4  15521  lgseisen  15522  lgsquadlem1  15525  lgsquad2lem1  15529  lgsquad3  15532  m1lgs  15533  2lgslem1a1  15534  2sqlem7  15569