Theorem syl22anc 1274

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 1271	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  5629  tfrexlem  6499  th3qlem1  6805  en2prd  6991  enpr2d  6996  ssenen  7036  phplem4dom  7047  phplem4on  7053  fiunsnnn  7069  findcard2sd  7080  unsnfi  7110  sbthlemi9  7163  endjusym  7294  endjudisj  7424  djuen  7425  ltanqg  7619  ltmnqg  7620  ltnnnq  7642  addcmpblnq0  7662  addlocprlemeqgt  7751  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  addcanprleml  7833  recexprlem1ssl  7852  caucvgprlemloc  7894  caucvgprprlemloccalc  7903  mulcmpblnr  7960  ltasrg  7989  recexgt0sr  7992  mulextsr1lem  7999  mulextsr1  8000  srpospr  8002  prsrlt  8006  ltpsrprg  8022  mappsrprg  8023  pitonnlem1p1  8065  recidpirq  8077  axpre-ltadd  8105  mulgt0d  8301  mul4d  8333  add4d  8347  add42d  8348  subcan  8433  addsub4d  8536  subadd4d  8537  sub4d  8538  2addsubd  8539  addsubeq4d  8540  muladdd  8594  mulsubd  8595  addgegt0d  8698  addgtge0d  8699  addge0d  8701  le2addd  8742  le2subd  8743  ltleaddd  8744  leltaddd  8745  lt2subd  8747  apreap  8766  apsym  8785  apcotr  8786  apadd1  8787  apneg  8790  mulext1  8791  mulap0r  8794  mulge0d  8800  mulap0d  8837  divdivdivap  8892  divcanap5  8893  divap0d  8985  recdivapd  8986  recdivap2d  8987  divcanap6d  8988  ddcanapd  8989  rec11apd  8990  divmuldivapd  9011  divmuleqapd  9012  subrecapd  9020  prodgt0  9031  lt2msq  9065  ledivdiv  9069  lediv12a  9073  recreclt  9079  divgt0d  9114  mulgt1d  9115  lemulge11d  9116  lemulge12d  9117  ltmul12ad  9120  lemul12ad  9121  lemul12bd  9122  nndivtr  9184  qreccl  9875  ledivdivd  9956  lediv12ad  9990  lt2mul2divd  9999  xlt2add  10114  xleaddadd  10121  iccss2  10178  iccssico2  10181  lincmb01cmp  10237  iccf1o  10238  fzrev2i  10320  qtri3or  10499  elicore  10525  2tnp1ge0ge0  10560  modqid  10610  q0mod  10616  q1mod  10617  modqabs  10618  modqadd1  10622  mulqaddmodid  10625  mulp1mod1  10626  modqmuladd  10627  modqmuladdnn0  10629  qnegmod  10630  m1modnnsub1  10631  addmodid  10633  modqm1p1mod0  10636  modqltm1p1mod  10637  modqmul1  10638  q2submod  10646  modifeq2int  10647  modaddmodup  10648  modaddmodlo  10649  modqaddmulmod  10652  modqsubdir  10654  modqeqmodmin  10655  modsumfzodifsn  10657  addmodlteq  10659  frecfzennn  10687  ser3mono  10748  expcl2lemap  10812  mulexpzap  10840  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  ltexp2a  10852  leexp2a  10853  sqdivap  10864  qsqeqor  10911  expnbnd  10924  expsubapd  10945  lt2sqd  10965  le2sqd  10966  sq11d  10967  apexp1  10979  bcp1nk  11023  hashunlem  11066  zfz1isolem1  11103  cjap  11466  cnreim  11538  resqrexlem1arp  11565  resqrexlemp1rp  11566  resqrexlemglsq  11582  abs00ap  11622  absext  11623  absexpzap  11640  absrele  11643  sqrtmuld  11729  sqrtsq2d  11730  sqrtled  11731  sqrtltd  11732  sqr11d  11733  abs3lemd  11761  minmax  11790  xrmaxiflemlub  11808  xrltmaxsup  11817  xrminmax  11825  xrbdtri  11836  climuni  11853  2clim  11861  addcn2  11870  mulcn2  11872  fsum3  11947  mptfzshft  12002  fsumrev  12003  fisum0diag2  12007  modfsummodlemstep  12017  binomlem  12043  mertenslemi1  12095  fprodrev  12179  efcllemp  12218  p1modz1  12354  dvds1  12413  dvdsext  12415  mulmoddvds  12423  oexpneg  12437  evennn02n  12442  evennn2n  12443  bitsinv1  12522  bezoutlemmo  12576  mulgcd  12586  dvdssqlem  12600  rpmulgcd2  12666  isprm6  12718  sqrt2irraplemnn  12750  sqrt2irrap  12751  crth  12795  eulerthlemh  12802  prmdiveq  12807  powm2modprm  12824  modprm0  12826  pythagtriplem2  12838  pythagtriplem11  12846  pythagtriplem13  12848  pythagtrip  12855  pcid  12896  pcgcd1  12900  pcprmpw2  12905  dvdsprmpweqle  12909  pcaddlem  12911  pcadd  12912  fldivp1  12920  4sqlem12  12974  4sqlem14  12976  4sqlem15  12977  4sqlem16  12978  unennn  13017  ennnfonelemg  13023  ennnfonelemhf1o  13033  inffinp1  13049  isstructr  13096  setscomd  13122  imasbas  13389  imasplusg  13390  imasmulr  13391  subm0  13564  lssvancl1  14380  lssvnegcl  14389  lspprvacl  14426  lspsneli  14428  lspsn  14429  znf1o  14664  ntrin  14847  topssnei  14885  restbasg  14891  cnntri  14947  txcn  14998  txlm  15002  cnmpt2res  15020  psmetlecl  15057  xmetlecl  15090  bldisj  15124  bdmet  15225  bdbl  15226  bdmopn  15227  xmetxp  15230  metcnp  15235  tgioo  15277  cncfmet  15315  dedekindeulemlub  15343  suplociccreex  15347  ellimc3apf  15383  limcimolemlt  15387  limccnp2cntop  15400  dvfvalap  15404  dvidsslem  15416  dvmulxxbr  15425  dvaddxx  15426  dvmulxx  15427  dviaddf  15428  dvimulf  15429  dvcoapbr  15430  dvmptclx  15441  cxplt3  15643  cxpltd  15651  cxpled  15652  cxplt3d  15658  cxple3d  15659  logbrec  15683  logbgcd1irraplemap  15692  wilthlem1  15703  mpodvdsmulf1o  15713  lgslem1  15728  lgslem3  15730  lgsdirprm  15762  gausslemma2dlem1f1o  15788  gausslemma2dlem6  15795  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem4  15801  lgseisen  15802  lgsquadlem1  15805  lgsquad2lem1  15809  lgsquad3  15812  m1lgs  15813  2lgslem1a1  15814  2sqlem7  15849  usgredg2v  16074  vtxd0nedgbfi  16149  clwwlknonex2  16289  gsumgfsumlem  16683