Theorem syl22anc 1274

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 1271	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  5629  tfrexlem  6500  th3qlem1  6806  en2prd  6992  enpr2d  6997  ssenen  7037  phplem4dom  7048  phplem4on  7054  fiunsnnn  7070  findcard2sd  7081  unsnfi  7111  sbthlemi9  7164  endjusym  7295  endjudisj  7425  djuen  7426  ltanqg  7620  ltmnqg  7621  ltnnnq  7643  addcmpblnq0  7663  addlocprlemeqgt  7752  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  addcanprleml  7834  recexprlem1ssl  7853  caucvgprlemloc  7895  caucvgprprlemloccalc  7904  mulcmpblnr  7961  ltasrg  7990  recexgt0sr  7993  mulextsr1lem  8000  mulextsr1  8001  srpospr  8003  prsrlt  8007  ltpsrprg  8023  mappsrprg  8024  pitonnlem1p1  8066  recidpirq  8078  axpre-ltadd  8106  mulgt0d  8302  mul4d  8334  add4d  8348  add42d  8349  subcan  8434  addsub4d  8537  subadd4d  8538  sub4d  8539  2addsubd  8540  addsubeq4d  8541  muladdd  8595  mulsubd  8596  addgegt0d  8699  addgtge0d  8700  addge0d  8702  le2addd  8743  le2subd  8744  ltleaddd  8745  leltaddd  8746  lt2subd  8748  apreap  8767  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  mulap0r  8795  mulge0d  8801  mulap0d  8838  divdivdivap  8893  divcanap5  8894  divap0d  8986  recdivapd  8987  recdivap2d  8988  divcanap6d  8989  ddcanapd  8990  rec11apd  8991  divmuldivapd  9012  divmuleqapd  9013  subrecapd  9021  prodgt0  9032  lt2msq  9066  ledivdiv  9070  lediv12a  9074  recreclt  9080  divgt0d  9115  mulgt1d  9116  lemulge11d  9117  lemulge12d  9118  ltmul12ad  9121  lemul12ad  9122  lemul12bd  9123  nndivtr  9185  qreccl  9876  ledivdivd  9957  lediv12ad  9991  lt2mul2divd  10000  xlt2add  10115  xleaddadd  10122  iccss2  10179  iccssico2  10182  lincmb01cmp  10238  iccf1o  10239  fzrev2i  10321  qtri3or  10501  elicore  10527  2tnp1ge0ge0  10562  modqid  10612  q0mod  10618  q1mod  10619  modqabs  10620  modqadd1  10624  mulqaddmodid  10627  mulp1mod1  10628  modqmuladd  10629  modqmuladdnn0  10631  qnegmod  10632  m1modnnsub1  10633  addmodid  10635  modqm1p1mod0  10638  modqltm1p1mod  10639  modqmul1  10640  q2submod  10648  modifeq2int  10649  modaddmodup  10650  modaddmodlo  10651  modqaddmulmod  10654  modqsubdir  10656  modqeqmodmin  10657  modsumfzodifsn  10659  addmodlteq  10661  frecfzennn  10689  ser3mono  10750  expcl2lemap  10814  mulexpzap  10842  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  ltexp2a  10854  leexp2a  10855  sqdivap  10866  qsqeqor  10913  expnbnd  10926  expsubapd  10947  lt2sqd  10967  le2sqd  10968  sq11d  10969  apexp1  10981  bcp1nk  11025  hashunlem  11068  zfz1isolem1  11105  hashtpgim  11110  cjap  11484  cnreim  11556  resqrexlem1arp  11583  resqrexlemp1rp  11584  resqrexlemglsq  11600  abs00ap  11640  absext  11641  absexpzap  11658  absrele  11661  sqrtmuld  11747  sqrtsq2d  11748  sqrtled  11749  sqrtltd  11750  sqr11d  11751  abs3lemd  11779  minmax  11808  xrmaxiflemlub  11826  xrltmaxsup  11835  xrminmax  11843  xrbdtri  11854  climuni  11871  2clim  11879  addcn2  11888  mulcn2  11890  fsum3  11966  mptfzshft  12021  fsumrev  12022  fisum0diag2  12026  modfsummodlemstep  12036  binomlem  12062  mertenslemi1  12114  fprodrev  12198  efcllemp  12237  p1modz1  12373  dvds1  12432  dvdsext  12434  mulmoddvds  12442  oexpneg  12456  evennn02n  12461  evennn2n  12462  bitsinv1  12541  bezoutlemmo  12595  mulgcd  12605  dvdssqlem  12619  rpmulgcd2  12685  isprm6  12737  sqrt2irraplemnn  12769  sqrt2irrap  12770  crth  12814  eulerthlemh  12821  prmdiveq  12826  powm2modprm  12843  modprm0  12845  pythagtriplem2  12857  pythagtriplem11  12865  pythagtriplem13  12867  pythagtrip  12874  pcid  12915  pcgcd1  12919  pcprmpw2  12924  dvdsprmpweqle  12928  pcaddlem  12930  pcadd  12931  fldivp1  12939  4sqlem12  12993  4sqlem14  12995  4sqlem15  12996  4sqlem16  12997  unennn  13036  ennnfonelemg  13042  ennnfonelemhf1o  13052  inffinp1  13068  isstructr  13115  setscomd  13141  imasbas  13408  imasplusg  13409  imasmulr  13410  subm0  13583  lssvancl1  14400  lssvnegcl  14409  lspprvacl  14446  lspsneli  14448  lspsn  14449  znf1o  14684  ntrin  14867  topssnei  14905  restbasg  14911  cnntri  14967  txcn  15018  txlm  15022  cnmpt2res  15040  psmetlecl  15077  xmetlecl  15110  bldisj  15144  bdmet  15245  bdbl  15246  bdmopn  15247  xmetxp  15250  metcnp  15255  tgioo  15297  cncfmet  15335  dedekindeulemlub  15363  suplociccreex  15367  ellimc3apf  15403  limcimolemlt  15407  limccnp2cntop  15420  dvfvalap  15424  dvidsslem  15436  dvmulxxbr  15445  dvaddxx  15446  dvmulxx  15447  dviaddf  15448  dvimulf  15449  dvcoapbr  15450  dvmptclx  15461  cxplt3  15663  cxpltd  15671  cxpled  15672  cxplt3d  15678  cxple3d  15679  logbrec  15703  logbgcd1irraplemap  15712  wilthlem1  15723  mpodvdsmulf1o  15733  lgslem1  15748  lgslem3  15750  lgsdirprm  15782  gausslemma2dlem1f1o  15808  gausslemma2dlem6  15815  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem4  15821  lgseisen  15822  lgsquadlem1  15825  lgsquad2lem1  15829  lgsquad3  15832  m1lgs  15833  2lgslem1a1  15834  2sqlem7  15869  usgredg2v  16094  vtxd0nedgbfi  16169  clwwlknonex2  16309  gsumgfsumlem  16735  gfsump1  16738