Theorem syl22anc 1251

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 1248	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  5584  tfrexlem  6438  th3qlem1  6742  en2prd  6928  enpr2d  6930  ssenen  6968  phplem4dom  6979  phplem4on  6985  fiunsnnn  6999  findcard2sd  7010  unsnfi  7037  sbthlemi9  7088  endjusym  7219  endjudisj  7348  djuen  7349  ltanqg  7543  ltmnqg  7544  ltnnnq  7566  addcmpblnq0  7586  addlocprlemeqgt  7675  distrlem1prl  7725  distrlem1pru  7726  distrlem4prl  7727  distrlem4pru  7728  addcanprleml  7757  recexprlem1ssl  7776  caucvgprlemloc  7818  caucvgprprlemloccalc  7827  mulcmpblnr  7884  ltasrg  7913  recexgt0sr  7916  mulextsr1lem  7923  mulextsr1  7924  srpospr  7926  prsrlt  7930  ltpsrprg  7946  mappsrprg  7947  pitonnlem1p1  7989  recidpirq  8001  axpre-ltadd  8029  mulgt0d  8225  mul4d  8257  add4d  8271  add42d  8272  subcan  8357  addsub4d  8460  subadd4d  8461  sub4d  8462  2addsubd  8463  addsubeq4d  8464  muladdd  8518  mulsubd  8519  addgegt0d  8622  addgtge0d  8623  addge0d  8625  le2addd  8666  le2subd  8667  ltleaddd  8668  leltaddd  8669  lt2subd  8671  apreap  8690  apsym  8709  apcotr  8710  apadd1  8711  apneg  8714  mulext1  8715  mulap0r  8718  mulge0d  8724  mulap0d  8761  divdivdivap  8816  divcanap5  8817  divap0d  8909  recdivapd  8910  recdivap2d  8911  divcanap6d  8912  ddcanapd  8913  rec11apd  8914  divmuldivapd  8935  divmuleqapd  8936  subrecapd  8944  prodgt0  8955  lt2msq  8989  ledivdiv  8993  lediv12a  8997  recreclt  9003  divgt0d  9038  mulgt1d  9039  lemulge11d  9040  lemulge12d  9041  ltmul12ad  9044  lemul12ad  9045  lemul12bd  9046  nndivtr  9108  qreccl  9793  ledivdivd  9874  lediv12ad  9908  lt2mul2divd  9917  xlt2add  10032  xleaddadd  10039  iccss2  10096  iccssico2  10099  lincmb01cmp  10155  iccf1o  10156  fzrev2i  10238  qtri3or  10415  elicore  10441  2tnp1ge0ge0  10476  modqid  10526  q0mod  10532  q1mod  10533  modqabs  10534  modqadd1  10538  mulqaddmodid  10541  mulp1mod1  10542  modqmuladd  10543  modqmuladdnn0  10545  qnegmod  10546  m1modnnsub1  10547  addmodid  10549  modqm1p1mod0  10552  modqltm1p1mod  10553  modqmul1  10554  q2submod  10562  modifeq2int  10563  modaddmodup  10564  modaddmodlo  10565  modqaddmulmod  10568  modqsubdir  10570  modqeqmodmin  10571  modsumfzodifsn  10573  addmodlteq  10575  frecfzennn  10603  ser3mono  10664  expcl2lemap  10728  mulexpzap  10756  expaddzaplem  10759  expaddzap  10760  expmulzap  10762  ltexp2a  10768  leexp2a  10769  sqdivap  10780  qsqeqor  10827  expnbnd  10840  expsubapd  10861  lt2sqd  10881  le2sqd  10882  sq11d  10883  apexp1  10895  bcp1nk  10939  hashunlem  10981  zfz1isolem1  11017  cjap  11302  cnreim  11374  resqrexlem1arp  11401  resqrexlemp1rp  11402  resqrexlemglsq  11418  abs00ap  11458  absext  11459  absexpzap  11476  absrele  11479  sqrtmuld  11565  sqrtsq2d  11566  sqrtled  11567  sqrtltd  11568  sqr11d  11569  abs3lemd  11597  minmax  11626  xrmaxiflemlub  11644  xrltmaxsup  11653  xrminmax  11661  xrbdtri  11672  climuni  11689  2clim  11697  addcn2  11706  mulcn2  11708  fsum3  11783  mptfzshft  11838  fsumrev  11839  fisum0diag2  11843  modfsummodlemstep  11853  binomlem  11879  mertenslemi1  11931  fprodrev  12015  efcllemp  12054  p1modz1  12190  dvds1  12249  dvdsext  12251  mulmoddvds  12259  oexpneg  12273  evennn02n  12278  evennn2n  12279  bitsinv1  12358  bezoutlemmo  12412  mulgcd  12422  dvdssqlem  12436  rpmulgcd2  12502  isprm6  12554  sqrt2irraplemnn  12586  sqrt2irrap  12587  crth  12631  eulerthlemh  12638  prmdiveq  12643  powm2modprm  12660  modprm0  12662  pythagtriplem2  12674  pythagtriplem11  12682  pythagtriplem13  12684  pythagtrip  12691  pcid  12732  pcgcd1  12736  pcprmpw2  12741  dvdsprmpweqle  12745  pcaddlem  12747  pcadd  12748  fldivp1  12756  4sqlem12  12810  4sqlem14  12812  4sqlem15  12813  4sqlem16  12814  unennn  12853  ennnfonelemg  12859  ennnfonelemhf1o  12869  inffinp1  12885  isstructr  12932  setscomd  12958  imasbas  13224  imasplusg  13225  imasmulr  13226  subm0  13399  lssvancl1  14214  lssvnegcl  14223  lspprvacl  14260  lspsneli  14262  lspsn  14263  znf1o  14498  ntrin  14681  topssnei  14719  restbasg  14725  cnntri  14781  txcn  14832  txlm  14836  cnmpt2res  14854  psmetlecl  14891  xmetlecl  14924  bldisj  14958  bdmet  15059  bdbl  15060  bdmopn  15061  xmetxp  15064  metcnp  15069  tgioo  15111  cncfmet  15149  dedekindeulemlub  15177  suplociccreex  15181  ellimc3apf  15217  limcimolemlt  15221  limccnp2cntop  15234  dvfvalap  15238  dvidsslem  15250  dvmulxxbr  15259  dvaddxx  15260  dvmulxx  15261  dviaddf  15262  dvimulf  15263  dvcoapbr  15264  dvmptclx  15275  cxplt3  15477  cxpltd  15485  cxpled  15486  cxplt3d  15492  cxple3d  15493  logbrec  15517  logbgcd1irraplemap  15526  wilthlem1  15537  mpodvdsmulf1o  15547  lgslem1  15562  lgslem3  15564  lgsdirprm  15596  gausslemma2dlem1f1o  15622  gausslemma2dlem6  15629  lgseisenlem1  15632  lgseisenlem2  15633  lgseisenlem4  15635  lgseisen  15636  lgsquadlem1  15639  lgsquad2lem1  15643  lgsquad3  15646  m1lgs  15647  2lgslem1a1  15648  2sqlem7  15683