Theorem syl22anc 1275

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 1272	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  5638  tfrexlem  6543  th3qlem1  6849  en2prd  7035  enpr2d  7040  ssenen  7080  phplem4dom  7091  phplem4on  7097  fiunsnnn  7113  findcard2sd  7124  unsnfi  7154  sbthlemi9  7207  endjusym  7338  endjudisj  7468  djuen  7469  ltanqg  7663  ltmnqg  7664  ltnnnq  7686  addcmpblnq0  7706  addlocprlemeqgt  7795  distrlem1prl  7845  distrlem1pru  7846  distrlem4prl  7847  distrlem4pru  7848  addcanprleml  7877  recexprlem1ssl  7896  caucvgprlemloc  7938  caucvgprprlemloccalc  7947  mulcmpblnr  8004  ltasrg  8033  recexgt0sr  8036  mulextsr1lem  8043  mulextsr1  8044  srpospr  8046  prsrlt  8050  ltpsrprg  8066  mappsrprg  8067  pitonnlem1p1  8109  recidpirq  8121  axpre-ltadd  8149  mulgt0d  8344  mul4d  8376  add4d  8390  add42d  8391  subcan  8476  addsub4d  8579  subadd4d  8580  sub4d  8581  2addsubd  8582  addsubeq4d  8583  muladdd  8637  mulsubd  8638  addgegt0d  8741  addgtge0d  8742  addge0d  8744  le2addd  8785  le2subd  8786  ltleaddd  8787  leltaddd  8788  lt2subd  8790  apreap  8809  apsym  8828  apcotr  8829  apadd1  8830  apneg  8833  mulext1  8834  mulap0r  8837  mulge0d  8843  mulap0d  8880  divdivdivap  8935  divcanap5  8936  divap0d  9028  recdivapd  9029  recdivap2d  9030  divcanap6d  9031  ddcanapd  9032  rec11apd  9033  divmuldivapd  9054  divmuleqapd  9055  subrecapd  9063  prodgt0  9074  lt2msq  9108  ledivdiv  9112  lediv12a  9116  recreclt  9122  divgt0d  9157  mulgt1d  9158  lemulge11d  9159  lemulge12d  9160  ltmul12ad  9163  lemul12ad  9164  lemul12bd  9165  nndivtr  9227  qreccl  9920  ledivdivd  10001  lediv12ad  10035  lt2mul2divd  10044  xlt2add  10159  xleaddadd  10166  iccss2  10223  iccssico2  10226  lincmb01cmp  10282  iccf1o  10284  fzrev2i  10366  qtri3or  10546  elicore  10572  2tnp1ge0ge0  10607  modqid  10657  q0mod  10663  q1mod  10664  modqabs  10665  modqadd1  10669  mulqaddmodid  10672  mulp1mod1  10673  modqmuladd  10674  modqmuladdnn0  10676  qnegmod  10677  m1modnnsub1  10678  addmodid  10680  modqm1p1mod0  10683  modqltm1p1mod  10684  modqmul1  10685  q2submod  10693  modifeq2int  10694  modaddmodup  10695  modaddmodlo  10696  modqaddmulmod  10699  modqsubdir  10701  modqeqmodmin  10702  modsumfzodifsn  10704  addmodlteq  10706  frecfzennn  10734  ser3mono  10795  expcl2lemap  10859  mulexpzap  10887  expaddzaplem  10890  expaddzap  10891  expmulzap  10893  ltexp2a  10899  leexp2a  10900  sqdivap  10911  qsqeqor  10958  expnbnd  10971  expsubapd  10992  lt2sqd  11012  le2sqd  11013  sq11d  11014  apexp1  11026  bcp1nk  11070  hashunlem  11113  zfz1isolem1  11150  hashtpgim  11155  cjap  11529  cnreim  11601  resqrexlem1arp  11628  resqrexlemp1rp  11629  resqrexlemglsq  11645  abs00ap  11685  absext  11686  absexpzap  11703  absrele  11706  sqrtmuld  11792  sqrtsq2d  11793  sqrtled  11794  sqrtltd  11795  sqr11d  11796  abs3lemd  11824  minmax  11853  xrmaxiflemlub  11871  xrltmaxsup  11880  xrminmax  11888  xrbdtri  11899  climuni  11916  2clim  11924  addcn2  11933  mulcn2  11935  fsum3  12011  mptfzshft  12066  fsumrev  12067  fisum0diag2  12071  modfsummodlemstep  12081  binomlem  12107  mertenslemi1  12159  fprodrev  12243  efcllemp  12282  p1modz1  12418  dvds1  12477  dvdsext  12479  mulmoddvds  12487  oexpneg  12501  evennn02n  12506  evennn2n  12507  bitsinv1  12586  bezoutlemmo  12640  mulgcd  12650  dvdssqlem  12664  rpmulgcd2  12730  isprm6  12782  sqrt2irraplemnn  12814  sqrt2irrap  12815  crth  12859  eulerthlemh  12866  prmdiveq  12871  powm2modprm  12888  modprm0  12890  pythagtriplem2  12902  pythagtriplem11  12910  pythagtriplem13  12912  pythagtrip  12919  pcid  12960  pcgcd1  12964  pcprmpw2  12969  dvdsprmpweqle  12973  pcaddlem  12975  pcadd  12976  fldivp1  12984  4sqlem12  13038  4sqlem14  13040  4sqlem15  13041  4sqlem16  13042  unennn  13081  ennnfonelemg  13087  ennnfonelemhf1o  13097  inffinp1  13113  isstructr  13160  setscomd  13186  imasbas  13453  imasplusg  13454  imasmulr  13455  subm0  13628  lssvancl1  14446  lssvnegcl  14455  lspprvacl  14492  lspsneli  14494  lspsn  14495  znf1o  14730  ntrin  14918  topssnei  14956  restbasg  14962  cnntri  15018  txcn  15069  txlm  15073  cnmpt2res  15091  psmetlecl  15128  xmetlecl  15161  bldisj  15195  bdmet  15296  bdbl  15297  bdmopn  15298  xmetxp  15301  metcnp  15306  tgioo  15348  cncfmet  15386  dedekindeulemlub  15414  suplociccreex  15418  ellimc3apf  15454  limcimolemlt  15458  limccnp2cntop  15471  dvfvalap  15475  dvidsslem  15487  dvmulxxbr  15496  dvaddxx  15497  dvmulxx  15498  dviaddf  15499  dvimulf  15500  dvcoapbr  15501  dvmptclx  15512  cxplt3  15714  cxpltd  15722  cxpled  15723  cxplt3d  15729  cxple3d  15730  logbrec  15754  logbgcd1irraplemap  15763  pellexlem1  15774  pellexlem2  15775  wilthlem1  15777  mpodvdsmulf1o  15787  lgslem1  15802  lgslem3  15804  lgsdirprm  15836  gausslemma2dlem1f1o  15862  gausslemma2dlem6  15869  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem4  15875  lgseisen  15876  lgsquadlem1  15879  lgsquad2lem1  15883  lgsquad3  15886  m1lgs  15887  2lgslem1a1  15888  2sqlem7  15923  usgredg2v  16148  vtxd0nedgbfi  16223  clwwlknonex2  16363  gsumgfsumlem  16795  gfsump1  16798