Theorem syl22anc 1239

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 1236	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  5505  tfrexlem  6334  th3qlem1  6636  enpr2d  6816  ssenen  6850  phplem4dom  6861  phplem4on  6866  fiunsnnn  6880  findcard2sd  6891  unsnfi  6917  sbthlemi9  6963  endjusym  7094  endjudisj  7208  djuen  7209  ltanqg  7398  ltmnqg  7399  ltnnnq  7421  addcmpblnq0  7441  addlocprlemeqgt  7530  distrlem1prl  7580  distrlem1pru  7581  distrlem4prl  7582  distrlem4pru  7583  addcanprleml  7612  recexprlem1ssl  7631  caucvgprlemloc  7673  caucvgprprlemloccalc  7682  mulcmpblnr  7739  ltasrg  7768  recexgt0sr  7771  mulextsr1lem  7778  mulextsr1  7779  srpospr  7781  prsrlt  7785  ltpsrprg  7801  mappsrprg  7802  pitonnlem1p1  7844  recidpirq  7856  axpre-ltadd  7884  mulgt0d  8079  mul4d  8111  add4d  8125  add42d  8126  subcan  8211  addsub4d  8314  subadd4d  8315  sub4d  8316  2addsubd  8317  addsubeq4d  8318  muladdd  8372  mulsubd  8373  addgegt0d  8475  addgtge0d  8476  addge0d  8478  le2addd  8519  le2subd  8520  ltleaddd  8521  leltaddd  8522  lt2subd  8524  apreap  8543  apsym  8562  apcotr  8563  apadd1  8564  apneg  8567  mulext1  8568  mulap0r  8571  mulge0d  8577  mulap0d  8614  divdivdivap  8669  divcanap5  8670  divap0d  8762  recdivapd  8763  recdivap2d  8764  divcanap6d  8765  ddcanapd  8766  rec11apd  8767  divmuldivapd  8788  divmuleqapd  8789  subrecapd  8797  prodgt0  8808  lt2msq  8842  ledivdiv  8846  lediv12a  8850  recreclt  8856  divgt0d  8891  mulgt1d  8892  lemulge11d  8893  lemulge12d  8894  ltmul12ad  8897  lemul12ad  8898  lemul12bd  8899  nndivtr  8960  qreccl  9641  ledivdivd  9721  lediv12ad  9755  lt2mul2divd  9764  xlt2add  9879  xleaddadd  9886  iccss2  9943  iccssico2  9946  lincmb01cmp  10002  iccf1o  10003  fzrev2i  10085  qtri3or  10242  elicore  10266  2tnp1ge0ge0  10300  modqid  10348  q0mod  10354  q1mod  10355  modqabs  10356  modqadd1  10360  mulqaddmodid  10363  mulp1mod1  10364  modqmuladd  10365  modqmuladdnn0  10367  qnegmod  10368  m1modnnsub1  10369  addmodid  10371  modqm1p1mod0  10374  modqltm1p1mod  10375  modqmul1  10376  q2submod  10384  modifeq2int  10385  modaddmodup  10386  modaddmodlo  10387  modqaddmulmod  10390  modqsubdir  10392  modqeqmodmin  10393  modsumfzodifsn  10395  addmodlteq  10397  frecfzennn  10425  ser3mono  10477  expcl2lemap  10531  mulexpzap  10559  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  ltexp2a  10571  leexp2a  10572  sqdivap  10583  qsqeqor  10630  expnbnd  10643  expsubapd  10664  lt2sqd  10684  le2sqd  10685  sq11d  10686  apexp1  10697  bcp1nk  10741  hashunlem  10783  zfz1isolem1  10819  cjap  10914  cnreim  10986  resqrexlem1arp  11013  resqrexlemp1rp  11014  resqrexlemglsq  11030  abs00ap  11070  absext  11071  absexpzap  11088  absrele  11091  sqrtmuld  11177  sqrtsq2d  11178  sqrtled  11179  sqrtltd  11180  sqr11d  11181  abs3lemd  11209  minmax  11237  xrmaxiflemlub  11255  xrltmaxsup  11264  xrminmax  11272  xrbdtri  11283  climuni  11300  2clim  11308  addcn2  11317  mulcn2  11319  fsum3  11394  mptfzshft  11449  fsumrev  11450  fisum0diag2  11454  modfsummodlemstep  11464  binomlem  11490  mertenslemi1  11542  fprodrev  11626  efcllemp  11665  p1modz1  11800  dvds1  11858  dvdsext  11860  mulmoddvds  11868  oexpneg  11881  evennn02n  11886  evennn2n  11887  bezoutlemmo  12006  mulgcd  12016  dvdssqlem  12030  rpmulgcd2  12094  isprm6  12146  sqrt2irraplemnn  12178  sqrt2irrap  12179  crth  12223  eulerthlemh  12230  prmdiveq  12235  powm2modprm  12251  modprm0  12253  pythagtriplem2  12265  pythagtriplem11  12273  pythagtriplem13  12275  pythagtrip  12282  pcid  12322  pcgcd1  12326  pcprmpw2  12331  dvdsprmpweqle  12335  pcaddlem  12337  pcadd  12338  fldivp1  12345  unennn  12397  ennnfonelemg  12403  ennnfonelemhf1o  12413  inffinp1  12429  isstructr  12476  setscomd  12502  imasbas  12727  imasplusg  12728  imasmulr  12729  ntrin  13594  topssnei  13632  restbasg  13638  cnntri  13694  txcn  13745  txlm  13749  cnmpt2res  13767  psmetlecl  13804  xmetlecl  13837  bldisj  13871  bdmet  13972  bdbl  13973  bdmopn  13974  xmetxp  13977  metcnp  13982  tgioo  14016  cncfmet  14049  dedekindeulemlub  14068  suplociccreex  14072  ellimc3apf  14099  limcimolemlt  14103  limccnp2cntop  14116  dvfvalap  14120  dvmulxxbr  14136  dvaddxx  14137  dvmulxx  14138  dviaddf  14139  dvimulf  14140  dvcoapbr  14141  dvmptclx  14150  cxplt3  14310  cxpltd  14318  cxpled  14319  cxplt3d  14324  cxple3d  14325  logbrec  14348  logbgcd1irraplemap  14357  lgslem1  14371  lgslem3  14373  lgsdirprm  14405  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2sqlem7  14438