Theorem syl22anc 1279

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 1276	1 |- ( ph -> et )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  f1oprg  5685  tfrexlem  6605  th3qlem1  6911  en2prd  7106  enpr2d  7111  ssenen  7152  phplem4dom  7163  phplem4on  7169  fiunsnnn  7185  findcard2sd  7196  unsnfi  7226  sbthlemi9  7282  fsuppcorn  7301  endjusym  7436  endjudisj  7566  djuen  7567  ltanqg  7767  ltmnqg  7768  ltnnnq  7790  addcmpblnq0  7810  addlocprlemeqgt  7899  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  addcanprleml  7981  recexprlem1ssl  8000  caucvgprlemloc  8042  caucvgprprlemloccalc  8051  mulcmpblnr  8108  ltasrg  8137  recexgt0sr  8140  mulextsr1lem  8147  mulextsr1  8148  srpospr  8150  prsrlt  8154  ltpsrprg  8170  mappsrprg  8171  pitonnlem1p1  8213  recidpirq  8225  axpre-ltadd  8253  mulgt0d  8449  mul4d  8481  add4d  8495  add42d  8496  subcan  8581  addsub4d  8684  subadd4d  8685  sub4d  8686  2addsubd  8687  addsubeq4d  8688  muladdd  8743  mulsubd  8744  addgegt0d  8847  addgtge0d  8848  addge0d  8850  le2addd  8891  le2subd  8892  ltleaddd  8893  leltaddd  8894  lt2subd  8896  apreap  8915  apsym  8934  apcotr  8935  apadd1  8936  apneg  8939  mulext1  8940  mulap0r  8943  mulge0d  8949  mulap0d  8986  divdivdivap  9043  divcanap5  9044  divap0d  9136  recdivapd  9137  recdivap2d  9138  divcanap6d  9139  ddcanapd  9140  rec11apd  9141  divmuldivapd  9162  divmuleqapd  9163  subrecapd  9171  prodgt0  9182  lt2msq  9216  ledivdiv  9220  lediv12a  9224  recreclt  9230  divgt0d  9265  mulgt1d  9266  lemulge11d  9267  lemulge12d  9268  ltmul12ad  9271  lemul12ad  9272  lemul12bd  9273  nndivtr  9346  qreccl  10042  ledivdivd  10123  lediv12ad  10157  lt2mul2divd  10166  xlt2add  10282  xleaddadd  10289  iccss2  10346  iccssico2  10349  lincmb01cmp  10405  iccf1o  10407  fzrev2i  10493  qtri3or  10675  elicore  10701  2tnp1ge0ge0  10736  modqid  10786  q0mod  10792  q1mod  10793  modqabs  10794  modqadd1  10798  mulqaddmodid  10801  mulp1mod1  10802  modqmuladd  10803  modqmuladdnn0  10805  qnegmod  10806  m1modnnsub1  10807  addmodid  10809  modqm1p1mod0  10812  modqltm1p1mod  10813  modqmul1  10814  q2submod  10822  modifeq2int  10823  modaddmodup  10824  modaddmodlo  10825  modqaddmulmod  10828  modqsubdir  10830  modqeqmodmin  10831  modsumfzodifsn  10833  addmodlteq  10835  frecfzennn  10863  ser3mono  10924  expcl2lemap  10988  mulexpzap  11016  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  ltexp2a  11028  leexp2a  11029  sqdivap  11040  qsqeqor  11087  expnbnd  11101  expsubapd  11122  lt2sqd  11142  le2sqd  11143  sq11d  11144  apexp1  11156  bcp1nk  11200  hashunlem  11244  hashf1lem1  11285  zfz1isolem1  11292  hashtpgim  11297  sq01  11660  cjap  11672  cnreim  11744  resqrexlem1arp  11771  resqrexlemp1rp  11772  resqrexlemglsq  11788  abs00ap  11828  absext  11829  absexpzap  11846  absrele  11849  sqrtmuld  11935  sqrtsq2d  11936  sqrtled  11937  sqrtltd  11938  sqr11d  11939  abs3lemd  11967  minmax  11996  xrmaxiflemlub  12014  xrltmaxsup  12023  xrminmax  12031  xrbdtri  12042  climuni  12059  2clim  12067  addcn2  12076  mulcn2  12078  fsum3  12154  mptfzshft  12209  fsumrev  12210  fisum0diag2  12214  modfsummodlemstep  12224  binomlem  12250  mertenslemi1  12302  fprodrev  12386  efcllemp  12425  p1modz1  12561  dvds1  12620  dvdsext  12622  mulmoddvds  12630  oexpneg  12644  evennn02n  12649  evennn2n  12650  bitsinv1  12729  bezoutlemmo  12783  mulgcd  12793  dvdssqlem  12807  rpmulgcd2  12873  isprm6  12925  sqrt2irraplemnn  12957  sqrt2irrap  12958  crth  13002  eulerthlemh  13009  prmdiveq  13014  powm2modprm  13031  modprm0  13033  pythagtriplem2  13045  pythagtriplem11  13053  pythagtriplem13  13055  pythagtrip  13062  pcid  13103  pcgcd1  13107  pcprmpw2  13112  dvdsprmpweqle  13116  pcaddlem  13118  pcadd  13119  fldivp1  13127  4sqlem12  13181  4sqlem14  13183  4sqlem15  13184  4sqlem16  13185  ballotfilemsima  13259  ballotfilemfrceq  13272  unennn  13288  ennnfonelemg  13294  ennnfonelemhf1o  13304  inffinp1  13320  isstructr  13367  setscomd  13393  imasbas  13628  imasplusg  13629  imasmulr  13630  subm0  13789  gzsumshift  14149  gsump1  14157  lssvancl1  14704  lssvnegcl  14713  lspprvacl  14750  lspsneli  14752  lspsn  14753  znf1o  14986  ntrin  15225  topssnei  15263  restbasg  15269  cnntri  15325  txcn  15376  txlm  15380  cnmpt2res  15398  psmetlecl  15435  xmetlecl  15468  bldisj  15502  bdmet  15603  bdbl  15604  bdmopn  15605  xmetxp  15608  metcnp  15613  tgioo  15655  cncfmet  15693  dedekindeulemlub  15721  suplociccreex  15725  ellimc3apf  15761  limcimolemlt  15765  limccnp2cntop  15778  dvfvalap  15782  dvidsslem  15794  dvmulxxbr  15803  dvaddxx  15804  dvmulxx  15805  dviaddf  15806  dvimulf  15807  dvcoapbr  15808  dvmptclx  15819  cxplt3  16022  cxpltd  16030  cxpled  16031  cxplt3d  16037  cxple3d  16038  logbrec  16062  logbgcd1irraplemap  16071  log2tlbndlog2  16082  birthdaylem3  16089  pellexlem1  16091  pellexlem2  16092  wilthlem1  16094  mpodvdsmulf1o  16104  lgslem1  16119  lgslem3  16121  lgsdirprm  16153  gausslemma2dlem1f1o  16179  gausslemma2dlem6  16186  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem4  16192  lgseisen  16193  lgsquadlem1  16196  lgsquad2lem1  16200  lgsquad3  16203  m1lgs  16204  2lgslem1a1  16205  2sqlem7  16240  usgredg2v  16465  vtxd0nedgbfi  16540  clwwlknonex2  16680