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  5551  tfrexlem  6401  th3qlem1  6705  enpr2d  6885  ssenen  6921  phplem4dom  6932  phplem4on  6937  fiunsnnn  6951  findcard2sd  6962  unsnfi  6989  sbthlemi9  7040  endjusym  7171  endjudisj  7293  djuen  7294  ltanqg  7484  ltmnqg  7485  ltnnnq  7507  addcmpblnq0  7527  addlocprlemeqgt  7616  distrlem1prl  7666  distrlem1pru  7667  distrlem4prl  7668  distrlem4pru  7669  addcanprleml  7698  recexprlem1ssl  7717  caucvgprlemloc  7759  caucvgprprlemloccalc  7768  mulcmpblnr  7825  ltasrg  7854  recexgt0sr  7857  mulextsr1lem  7864  mulextsr1  7865  srpospr  7867  prsrlt  7871  ltpsrprg  7887  mappsrprg  7888  pitonnlem1p1  7930  recidpirq  7942  axpre-ltadd  7970  mulgt0d  8166  mul4d  8198  add4d  8212  add42d  8213  subcan  8298  addsub4d  8401  subadd4d  8402  sub4d  8403  2addsubd  8404  addsubeq4d  8405  muladdd  8459  mulsubd  8460  addgegt0d  8563  addgtge0d  8564  addge0d  8566  le2addd  8607  le2subd  8608  ltleaddd  8609  leltaddd  8610  lt2subd  8612  apreap  8631  apsym  8650  apcotr  8651  apadd1  8652  apneg  8655  mulext1  8656  mulap0r  8659  mulge0d  8665  mulap0d  8702  divdivdivap  8757  divcanap5  8758  divap0d  8850  recdivapd  8851  recdivap2d  8852  divcanap6d  8853  ddcanapd  8854  rec11apd  8855  divmuldivapd  8876  divmuleqapd  8877  subrecapd  8885  prodgt0  8896  lt2msq  8930  ledivdiv  8934  lediv12a  8938  recreclt  8944  divgt0d  8979  mulgt1d  8980  lemulge11d  8981  lemulge12d  8982  ltmul12ad  8985  lemul12ad  8986  lemul12bd  8987  nndivtr  9049  qreccl  9733  ledivdivd  9814  lediv12ad  9848  lt2mul2divd  9857  xlt2add  9972  xleaddadd  9979  iccss2  10036  iccssico2  10039  lincmb01cmp  10095  iccf1o  10096  fzrev2i  10178  qtri3or  10347  elicore  10373  2tnp1ge0ge0  10408  modqid  10458  q0mod  10464  q1mod  10465  modqabs  10466  modqadd1  10470  mulqaddmodid  10473  mulp1mod1  10474  modqmuladd  10475  modqmuladdnn0  10477  qnegmod  10478  m1modnnsub1  10479  addmodid  10481  modqm1p1mod0  10484  modqltm1p1mod  10485  modqmul1  10486  q2submod  10494  modifeq2int  10495  modaddmodup  10496  modaddmodlo  10497  modqaddmulmod  10500  modqsubdir  10502  modqeqmodmin  10503  modsumfzodifsn  10505  addmodlteq  10507  frecfzennn  10535  ser3mono  10596  expcl2lemap  10660  mulexpzap  10688  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  ltexp2a  10700  leexp2a  10701  sqdivap  10712  qsqeqor  10759  expnbnd  10772  expsubapd  10793  lt2sqd  10813  le2sqd  10814  sq11d  10815  apexp1  10827  bcp1nk  10871  hashunlem  10913  zfz1isolem1  10949  cjap  11088  cnreim  11160  resqrexlem1arp  11187  resqrexlemp1rp  11188  resqrexlemglsq  11204  abs00ap  11244  absext  11245  absexpzap  11262  absrele  11265  sqrtmuld  11351  sqrtsq2d  11352  sqrtled  11353  sqrtltd  11354  sqr11d  11355  abs3lemd  11383  minmax  11412  xrmaxiflemlub  11430  xrltmaxsup  11439  xrminmax  11447  xrbdtri  11458  climuni  11475  2clim  11483  addcn2  11492  mulcn2  11494  fsum3  11569  mptfzshft  11624  fsumrev  11625  fisum0diag2  11629  modfsummodlemstep  11639  binomlem  11665  mertenslemi1  11717  fprodrev  11801  efcllemp  11840  p1modz1  11976  dvds1  12035  dvdsext  12037  mulmoddvds  12045  oexpneg  12059  evennn02n  12064  evennn2n  12065  bitsinv1  12144  bezoutlemmo  12198  mulgcd  12208  dvdssqlem  12222  rpmulgcd2  12288  isprm6  12340  sqrt2irraplemnn  12372  sqrt2irrap  12373  crth  12417  eulerthlemh  12424  prmdiveq  12429  powm2modprm  12446  modprm0  12448  pythagtriplem2  12460  pythagtriplem11  12468  pythagtriplem13  12470  pythagtrip  12477  pcid  12518  pcgcd1  12522  pcprmpw2  12527  dvdsprmpweqle  12531  pcaddlem  12533  pcadd  12534  fldivp1  12542  4sqlem12  12596  4sqlem14  12598  4sqlem15  12599  4sqlem16  12600  unennn  12639  ennnfonelemg  12645  ennnfonelemhf1o  12655  inffinp1  12671  isstructr  12718  setscomd  12744  imasbas  13009  imasplusg  13010  imasmulr  13011  subm0  13184  lssvancl1  13999  lssvnegcl  14008  lspprvacl  14045  lspsneli  14047  lspsn  14048  znf1o  14283  ntrin  14444  topssnei  14482  restbasg  14488  cnntri  14544  txcn  14595  txlm  14599  cnmpt2res  14617  psmetlecl  14654  xmetlecl  14687  bldisj  14721  bdmet  14822  bdbl  14823  bdmopn  14824  xmetxp  14827  metcnp  14832  tgioo  14874  cncfmet  14912  dedekindeulemlub  14940  suplociccreex  14944  ellimc3apf  14980  limcimolemlt  14984  limccnp2cntop  14997  dvfvalap  15001  dvidsslem  15013  dvmulxxbr  15022  dvaddxx  15023  dvmulxx  15024  dviaddf  15025  dvimulf  15026  dvcoapbr  15027  dvmptclx  15038  cxplt3  15240  cxpltd  15248  cxpled  15249  cxplt3d  15255  cxple3d  15256  logbrec  15280  logbgcd1irraplemap  15289  wilthlem1  15300  mpodvdsmulf1o  15310  lgslem1  15325  lgslem3  15327  lgsdirprm  15359  gausslemma2dlem1f1o  15385  gausslemma2dlem6  15392  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem4  15398  lgseisen  15399  lgsquadlem1  15402  lgsquad2lem1  15406  lgsquad3  15409  m1lgs  15410  2lgslem1a1  15411  2sqlem7  15446