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  11159  cnreim  11231  resqrexlem1arp  11258  resqrexlemp1rp  11259  resqrexlemglsq  11275  abs00ap  11315  absext  11316  absexpzap  11333  absrele  11336  sqrtmuld  11422  sqrtsq2d  11423  sqrtled  11424  sqrtltd  11425  sqr11d  11426  abs3lemd  11454  minmax  11483  xrmaxiflemlub  11501  xrltmaxsup  11510  xrminmax  11518  xrbdtri  11529  climuni  11546  2clim  11554  addcn2  11563  mulcn2  11565  fsum3  11640  mptfzshft  11695  fsumrev  11696  fisum0diag2  11700  modfsummodlemstep  11710  binomlem  11736  mertenslemi1  11788  fprodrev  11872  efcllemp  11911  p1modz1  12047  dvds1  12106  dvdsext  12108  mulmoddvds  12116  oexpneg  12130  evennn02n  12135  evennn2n  12136  bitsinv1  12215  bezoutlemmo  12269  mulgcd  12279  dvdssqlem  12293  rpmulgcd2  12359  isprm6  12411  sqrt2irraplemnn  12443  sqrt2irrap  12444  crth  12488  eulerthlemh  12495  prmdiveq  12500  powm2modprm  12517  modprm0  12519  pythagtriplem2  12531  pythagtriplem11  12539  pythagtriplem13  12541  pythagtrip  12548  pcid  12589  pcgcd1  12593  pcprmpw2  12598  dvdsprmpweqle  12602  pcaddlem  12604  pcadd  12605  fldivp1  12613  4sqlem12  12667  4sqlem14  12669  4sqlem15  12670  4sqlem16  12671  unennn  12710  ennnfonelemg  12716  ennnfonelemhf1o  12726  inffinp1  12742  isstructr  12789  setscomd  12815  imasbas  13081  imasplusg  13082  imasmulr  13083  subm0  13256  lssvancl1  14071  lssvnegcl  14080  lspprvacl  14117  lspsneli  14119  lspsn  14120  znf1o  14355  ntrin  14538  topssnei  14576  restbasg  14582  cnntri  14638  txcn  14689  txlm  14693  cnmpt2res  14711  psmetlecl  14748  xmetlecl  14781  bldisj  14815  bdmet  14916  bdbl  14917  bdmopn  14918  xmetxp  14921  metcnp  14926  tgioo  14968  cncfmet  15006  dedekindeulemlub  15034  suplociccreex  15038  ellimc3apf  15074  limcimolemlt  15078  limccnp2cntop  15091  dvfvalap  15095  dvidsslem  15107  dvmulxxbr  15116  dvaddxx  15117  dvmulxx  15118  dviaddf  15119  dvimulf  15120  dvcoapbr  15121  dvmptclx  15132  cxplt3  15334  cxpltd  15342  cxpled  15343  cxplt3d  15349  cxple3d  15350  logbrec  15374  logbgcd1irraplemap  15383  wilthlem1  15394  mpodvdsmulf1o  15404  lgslem1  15419  lgslem3  15421  lgsdirprm  15453  gausslemma2dlem1f1o  15479  gausslemma2dlem6  15486  lgseisenlem1  15489  lgseisenlem2  15490  lgseisenlem4  15492  lgseisen  15493  lgsquadlem1  15496  lgsquad2lem1  15500  lgsquad3  15503  m1lgs  15504  2lgslem1a1  15505  2sqlem7  15540