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  8078  mul4d  8110  add4d  8124  add42d  8125  subcan  8210  addsub4d  8313  subadd4d  8314  sub4d  8315  2addsubd  8316  addsubeq4d  8317  muladdd  8371  mulsubd  8372  addgegt0d  8474  addgtge0d  8475  addge0d  8477  le2addd  8518  le2subd  8519  ltleaddd  8520  leltaddd  8521  lt2subd  8523  apreap  8542  apsym  8561  apcotr  8562  apadd1  8563  apneg  8566  mulext1  8567  mulap0r  8570  mulge0d  8576  mulap0d  8613  divdivdivap  8668  divcanap5  8669  divap0d  8761  recdivapd  8762  recdivap2d  8763  divcanap6d  8764  ddcanapd  8765  rec11apd  8766  divmuldivapd  8787  divmuleqapd  8788  subrecapd  8796  prodgt0  8807  lt2msq  8841  ledivdiv  8845  lediv12a  8849  recreclt  8855  divgt0d  8890  mulgt1d  8891  lemulge11d  8892  lemulge12d  8893  ltmul12ad  8896  lemul12ad  8897  lemul12bd  8898  nndivtr  8959  qreccl  9640  ledivdivd  9720  lediv12ad  9754  lt2mul2divd  9763  xlt2add  9878  xleaddadd  9885  iccss2  9942  iccssico2  9945  lincmb01cmp  10001  iccf1o  10002  fzrev2i  10083  qtri3or  10240  elicore  10264  2tnp1ge0ge0  10298  modqid  10346  q0mod  10352  q1mod  10353  modqabs  10354  modqadd1  10358  mulqaddmodid  10361  mulp1mod1  10362  modqmuladd  10363  modqmuladdnn0  10365  qnegmod  10366  m1modnnsub1  10367  addmodid  10369  modqm1p1mod0  10372  modqltm1p1mod  10373  modqmul1  10374  q2submod  10382  modifeq2int  10383  modaddmodup  10384  modaddmodlo  10385  modqaddmulmod  10388  modqsubdir  10390  modqeqmodmin  10391  modsumfzodifsn  10393  addmodlteq  10395  frecfzennn  10423  ser3mono  10475  expcl2lemap  10529  mulexpzap  10557  expaddzaplem  10560  expaddzap  10561  expmulzap  10563  ltexp2a  10569  leexp2a  10570  sqdivap  10581  qsqeqor  10627  expnbnd  10640  expsubapd  10661  lt2sqd  10681  le2sqd  10682  sq11d  10683  apexp1  10693  bcp1nk  10737  hashunlem  10779  zfz1isolem1  10815  cjap  10910  cnreim  10982  resqrexlem1arp  11009  resqrexlemp1rp  11010  resqrexlemglsq  11026  abs00ap  11066  absext  11067  absexpzap  11084  absrele  11087  sqrtmuld  11173  sqrtsq2d  11174  sqrtled  11175  sqrtltd  11176  sqr11d  11177  abs3lemd  11205  minmax  11233  xrmaxiflemlub  11251  xrltmaxsup  11260  xrminmax  11268  xrbdtri  11279  climuni  11296  2clim  11304  addcn2  11313  mulcn2  11315  fsum3  11390  mptfzshft  11445  fsumrev  11446  fisum0diag2  11450  modfsummodlemstep  11460  binomlem  11486  mertenslemi1  11538  fprodrev  11622  efcllemp  11661  p1modz1  11796  dvds1  11853  dvdsext  11855  mulmoddvds  11863  oexpneg  11876  evennn02n  11881  evennn2n  11882  bezoutlemmo  12001  mulgcd  12011  dvdssqlem  12025  rpmulgcd2  12089  isprm6  12141  sqrt2irraplemnn  12173  sqrt2irrap  12174  crth  12218  eulerthlemh  12225  prmdiveq  12230  powm2modprm  12246  modprm0  12248  pythagtriplem2  12260  pythagtriplem11  12268  pythagtriplem13  12270  pythagtrip  12277  pcid  12317  pcgcd1  12321  pcprmpw2  12326  dvdsprmpweqle  12330  pcaddlem  12332  pcadd  12333  fldivp1  12340  unennn  12392  ennnfonelemg  12398  ennnfonelemhf1o  12408  inffinp1  12424  isstructr  12471  setscomd  12497  imasbas  12722  imasplusg  12723  imasmulr  12724  ntrin  13555  topssnei  13593  restbasg  13599  cnntri  13655  txcn  13706  txlm  13710  cnmpt2res  13728  psmetlecl  13765  xmetlecl  13798  bldisj  13832  bdmet  13933  bdbl  13934  bdmopn  13935  xmetxp  13938  metcnp  13943  tgioo  13977  cncfmet  14010  dedekindeulemlub  14029  suplociccreex  14033  ellimc3apf  14060  limcimolemlt  14064  limccnp2cntop  14077  dvfvalap  14081  dvmulxxbr  14097  dvaddxx  14098  dvmulxx  14099  dviaddf  14100  dvimulf  14101  dvcoapbr  14102  dvmptclx  14111  cxplt3  14271  cxpltd  14279  cxpled  14280  cxplt3d  14285  cxple3d  14286  logbrec  14309  logbgcd1irraplemap  14318  lgslem1  14332  lgslem3  14334  lgsdirprm  14366  2sqlem7  14388