Theorem syl22anc 1272

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 1269	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  5619  tfrexlem  6486  th3qlem1  6792  en2prd  6978  enpr2d  6980  ssenen  7020  phplem4dom  7031  phplem4on  7037  fiunsnnn  7051  findcard2sd  7062  unsnfi  7092  sbthlemi9  7143  endjusym  7274  endjudisj  7403  djuen  7404  ltanqg  7598  ltmnqg  7599  ltnnnq  7621  addcmpblnq0  7641  addlocprlemeqgt  7730  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  addcanprleml  7812  recexprlem1ssl  7831  caucvgprlemloc  7873  caucvgprprlemloccalc  7882  mulcmpblnr  7939  ltasrg  7968  recexgt0sr  7971  mulextsr1lem  7978  mulextsr1  7979  srpospr  7981  prsrlt  7985  ltpsrprg  8001  mappsrprg  8002  pitonnlem1p1  8044  recidpirq  8056  axpre-ltadd  8084  mulgt0d  8280  mul4d  8312  add4d  8326  add42d  8327  subcan  8412  addsub4d  8515  subadd4d  8516  sub4d  8517  2addsubd  8518  addsubeq4d  8519  muladdd  8573  mulsubd  8574  addgegt0d  8677  addgtge0d  8678  addge0d  8680  le2addd  8721  le2subd  8722  ltleaddd  8723  leltaddd  8724  lt2subd  8726  apreap  8745  apsym  8764  apcotr  8765  apadd1  8766  apneg  8769  mulext1  8770  mulap0r  8773  mulge0d  8779  mulap0d  8816  divdivdivap  8871  divcanap5  8872  divap0d  8964  recdivapd  8965  recdivap2d  8966  divcanap6d  8967  ddcanapd  8968  rec11apd  8969  divmuldivapd  8990  divmuleqapd  8991  subrecapd  8999  prodgt0  9010  lt2msq  9044  ledivdiv  9048  lediv12a  9052  recreclt  9058  divgt0d  9093  mulgt1d  9094  lemulge11d  9095  lemulge12d  9096  ltmul12ad  9099  lemul12ad  9100  lemul12bd  9101  nndivtr  9163  qreccl  9849  ledivdivd  9930  lediv12ad  9964  lt2mul2divd  9973  xlt2add  10088  xleaddadd  10095  iccss2  10152  iccssico2  10155  lincmb01cmp  10211  iccf1o  10212  fzrev2i  10294  qtri3or  10472  elicore  10498  2tnp1ge0ge0  10533  modqid  10583  q0mod  10589  q1mod  10590  modqabs  10591  modqadd1  10595  mulqaddmodid  10598  mulp1mod1  10599  modqmuladd  10600  modqmuladdnn0  10602  qnegmod  10603  m1modnnsub1  10604  addmodid  10606  modqm1p1mod0  10609  modqltm1p1mod  10610  modqmul1  10611  q2submod  10619  modifeq2int  10620  modaddmodup  10621  modaddmodlo  10622  modqaddmulmod  10625  modqsubdir  10627  modqeqmodmin  10628  modsumfzodifsn  10630  addmodlteq  10632  frecfzennn  10660  ser3mono  10721  expcl2lemap  10785  mulexpzap  10813  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  ltexp2a  10825  leexp2a  10826  sqdivap  10837  qsqeqor  10884  expnbnd  10897  expsubapd  10918  lt2sqd  10938  le2sqd  10939  sq11d  10940  apexp1  10952  bcp1nk  10996  hashunlem  11038  zfz1isolem1  11075  cjap  11432  cnreim  11504  resqrexlem1arp  11531  resqrexlemp1rp  11532  resqrexlemglsq  11548  abs00ap  11588  absext  11589  absexpzap  11606  absrele  11609  sqrtmuld  11695  sqrtsq2d  11696  sqrtled  11697  sqrtltd  11698  sqr11d  11699  abs3lemd  11727  minmax  11756  xrmaxiflemlub  11774  xrltmaxsup  11783  xrminmax  11791  xrbdtri  11802  climuni  11819  2clim  11827  addcn2  11836  mulcn2  11838  fsum3  11913  mptfzshft  11968  fsumrev  11969  fisum0diag2  11973  modfsummodlemstep  11983  binomlem  12009  mertenslemi1  12061  fprodrev  12145  efcllemp  12184  p1modz1  12320  dvds1  12379  dvdsext  12381  mulmoddvds  12389  oexpneg  12403  evennn02n  12408  evennn2n  12409  bitsinv1  12488  bezoutlemmo  12542  mulgcd  12552  dvdssqlem  12566  rpmulgcd2  12632  isprm6  12684  sqrt2irraplemnn  12716  sqrt2irrap  12717  crth  12761  eulerthlemh  12768  prmdiveq  12773  powm2modprm  12790  modprm0  12792  pythagtriplem2  12804  pythagtriplem11  12812  pythagtriplem13  12814  pythagtrip  12821  pcid  12862  pcgcd1  12866  pcprmpw2  12871  dvdsprmpweqle  12875  pcaddlem  12877  pcadd  12878  fldivp1  12886  4sqlem12  12940  4sqlem14  12942  4sqlem15  12943  4sqlem16  12944  unennn  12983  ennnfonelemg  12989  ennnfonelemhf1o  12999  inffinp1  13015  isstructr  13062  setscomd  13088  imasbas  13355  imasplusg  13356  imasmulr  13357  subm0  13530  lssvancl1  14346  lssvnegcl  14355  lspprvacl  14392  lspsneli  14394  lspsn  14395  znf1o  14630  ntrin  14813  topssnei  14851  restbasg  14857  cnntri  14913  txcn  14964  txlm  14968  cnmpt2res  14986  psmetlecl  15023  xmetlecl  15056  bldisj  15090  bdmet  15191  bdbl  15192  bdmopn  15193  xmetxp  15196  metcnp  15201  tgioo  15243  cncfmet  15281  dedekindeulemlub  15309  suplociccreex  15313  ellimc3apf  15349  limcimolemlt  15353  limccnp2cntop  15366  dvfvalap  15370  dvidsslem  15382  dvmulxxbr  15391  dvaddxx  15392  dvmulxx  15393  dviaddf  15394  dvimulf  15395  dvcoapbr  15396  dvmptclx  15407  cxplt3  15609  cxpltd  15617  cxpled  15618  cxplt3d  15624  cxple3d  15625  logbrec  15649  logbgcd1irraplemap  15658  wilthlem1  15669  mpodvdsmulf1o  15679  lgslem1  15694  lgslem3  15696  lgsdirprm  15728  gausslemma2dlem1f1o  15754  gausslemma2dlem6  15761  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem4  15767  lgseisen  15768  lgsquadlem1  15771  lgsquad2lem1  15775  lgsquad3  15778  m1lgs  15779  2lgslem1a1  15780  2sqlem7  15815  usgredg2v  16037