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  8450  mul4d  8482  add4d  8496  add42d  8497  subcan  8582  addsub4d  8685  subadd4d  8686  sub4d  8687  2addsubd  8688  addsubeq4d  8689  muladdd  8744  mulsubd  8745  addgegt0d  8848  addgtge0d  8849  addge0d  8851  le2addd  8893  le2subd  8894  ltleaddd  8895  leltaddd  8896  lt2subd  8898  apreap  8917  apsym  8936  apcotr  8937  apadd1  8938  apneg  8941  mulext1  8942  mulap0r  8945  mulge0d  8951  mulap0d  8988  divdivdivap  9045  divcanap5  9046  divap0d  9138  recdivapd  9139  recdivap2d  9140  divcanap6d  9141  ddcanapd  9142  rec11apd  9143  divmuldivapd  9164  divmuleqapd  9165  subrecapd  9173  prodgt0  9184  lt2msq  9218  ledivdiv  9222  lediv12a  9226  recreclt  9232  divgt0d  9267  mulgt1d  9268  lemulge11d  9269  lemulge12d  9270  ltmul12ad  9273  lemul12ad  9274  lemul12bd  9275  nndivtr  9348  qreccl  10051  ledivdivd  10133  lediv12ad  10167  lt2mul2divd  10176  xlt2add  10292  xleaddadd  10299  iccss2  10356  iccssico2  10359  lincmb01cmp  10415  iccf1o  10417  fzrev2i  10503  qtri3or  10685  elicore  10711  2tnp1ge0ge0  10749  modqid  10799  q0mod  10805  q1mod  10806  modqabs  10807  modqadd1  10811  mulqaddmodid  10814  mulp1mod1  10815  modqmuladd  10816  modqmuladdnn0  10818  qnegmod  10819  m1modnnsub1  10820  addmodid  10822  modqm1p1mod0  10825  modqltm1p1mod  10826  modqmul1  10827  q2submod  10835  modifeq2int  10836  modaddmodup  10837  modaddmodlo  10838  modqaddmulmod  10841  modqsubdir  10843  modqeqmodmin  10844  modsumfzodifsn  10846  addmodlteq  10848  frecfzennn  10876  ser3mono  10937  expcl2lemap  11001  mulexpzap  11029  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  ltexp2a  11041  leexp2a  11042  sqdivap  11053  qsqeqor  11100  expnbnd  11114  expsubapd  11135  lt2sqd  11155  le2sqd  11156  sq11d  11157  apexp1  11170  bcp1nk  11214  hashunlem  11258  hashf1lem1  11299  zfz1isolem1  11306  hashtpgim  11311  sq01  11674  cjap  11686  cnreim  11758  resqrexlem1arp  11785  resqrexlemp1rp  11786  resqrexlemglsq  11802  abs00ap  11842  absext  11843  absexpzap  11861  absrele  11864  sqrtmuld  11950  sqrtsq2d  11951  sqrtled  11952  sqrtltd  11953  sqr11d  11954  abs3lemd  11982  minmax  12011  xrmaxiflemlub  12030  xrltmaxsup  12039  xrminmax  12047  xrbdtri  12058  climuni  12075  2clim  12083  addcn2  12092  mulcn2  12094  fsum3  12170  mptfzshft  12225  fsumrev  12226  fisum0diag2  12230  modfsummodlemstep  12240  binomlem  12266  mertenslemi1  12318  fprodrev  12402  efcllemp  12441  p1modz1  12577  dvds1  12636  dvdsext  12638  mulmoddvds  12646  oexpneg  12660  evennn02n  12665  evennn2n  12666  bitsinv1  12745  bezoutlemmo  12799  mulgcd  12809  dvdssqlem  12823  rpmulgcd2  12889  isprm6  12942  sqrt2irraplemnn  12975  sqrt2irrap  12976  sqrtrirr  13005  crth  13022  eulerthlemh  13029  prmdiveq  13034  powm2modprm  13051  modprm0  13053  pythagtriplem2  13065  pythagtriplem11  13073  pythagtriplem13  13075  pythagtrip  13082  pcid  13123  pcgcd1  13127  pcprmpw2  13132  dvdsprmpweqle  13136  pcaddlem  13138  pcadd  13139  fldivp1  13147  4sqlem12  13201  4sqlem14  13203  4sqlem15  13204  4sqlem16  13205  ballotfilemsima  13308  ballotfilemfrceq  13321  unennn  13337  ennnfonelemg  13343  ennnfonelemhf1o  13353  inffinp1  13369  isstructr  13416  setscomd  13442  imasbas  13677  imasplusg  13678  imasmulr  13679  subm0  13838  gzsumshift  14198  gsump1  14206  lssvancl1  14753  lssvnegcl  14762  lspprvacl  14799  lspsneli  14801  lspsn  14802  znf1o  15035  ntrin  15274  topssnei  15312  restbasg  15318  cnntri  15374  txcn  15425  txlm  15429  cnmpt2res  15447  psmetlecl  15484  xmetlecl  15517  bldisj  15551  bdmet  15652  bdbl  15653  bdmopn  15654  xmetxp  15657  metcnp  15662  tgioo  15704  cncfmet  15742  dedekindeulemlub  15770  suplociccreex  15774  ellimc3apf  15810  limcimolemlt  15814  limccnp2cntop  15827  dvfvalap  15831  dvidsslem  15843  dvmulxxbr  15852  dvaddxx  15853  dvmulxx  15854  dviaddf  15855  dvimulf  15856  dvcoapbr  15857  dvmptclx  15868  cxplt3  16075  cxpltd  16083  cxpled  16084  cxplt3d  16090  cxple3d  16091  logbrec  16115  logbgcd1irraplemap  16124  zprmlogbaplem1  16134  log2tlbndlog2  16139  birthdaylem3  16146  pellexlem1  16148  pellexlem2  16149  wilthlem1  16151  ppiqsval  16156  ppiqwordi  16174  mpodvdsmulf1o  16185  ppiqub  16194  bclbnd  16205  lgslem1  16217  lgslem3  16219  lgsdirprm  16251  gausslemma2dlem1f1o  16277  gausslemma2dlem6  16284  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem4  16290  lgseisen  16291  lgsquadlem1  16294  lgsquad2lem1  16298  lgsquad3  16301  m1lgs  16302  2lgslem1a1  16303  2sqlem7  16338  usgredg2v  16563  vtxd0nedgbfi  16638  clwwlknonex2  16778