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  5688  tfrexlem  6609  th3qlem1  6915  en2prd  7110  enpr2d  7115  ssenen  7156  phplem4dom  7167  phplem4on  7173  fiunsnnn  7189  findcard2sd  7200  unsnfi  7230  sbthlemi9  7287  fsuppcorn  7306  endjusym  7442  endjudisj  7572  djuen  7573  ltanqg  7773  ltmnqg  7774  ltnnnq  7796  addcmpblnq0  7816  addlocprlemeqgt  7905  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  addcanprleml  7987  recexprlem1ssl  8006  caucvgprlemloc  8048  caucvgprprlemloccalc  8057  mulcmpblnr  8114  ltasrg  8143  recexgt0sr  8146  mulextsr1lem  8153  mulextsr1  8154  srpospr  8156  prsrlt  8160  ltpsrprg  8176  mappsrprg  8177  pitonnlem1p1  8219  recidpirq  8231  axpre-ltadd  8259  mulgt0d  8456  mul4d  8488  add4d  8502  add42d  8503  subcan  8588  addsub4d  8691  subadd4d  8692  sub4d  8693  2addsubd  8694  addsubeq4d  8695  muladdd  8750  mulsubd  8751  addgegt0d  8854  addgtge0d  8855  addge0d  8857  le2addd  8899  le2subd  8900  ltleaddd  8901  leltaddd  8902  lt2subd  8904  apreap  8923  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  mulap0r  8951  mulge0d  8957  mulap0d  8994  divdivdivap  9051  divcanap5  9052  divap0d  9144  recdivapd  9145  recdivap2d  9146  divcanap6d  9147  ddcanapd  9148  rec11apd  9149  divmuldivapd  9170  divmuleqapd  9171  subrecapd  9179  prodgt0  9190  lt2msq  9224  ledivdiv  9228  lediv12a  9232  recreclt  9238  divgt0d  9273  mulgt1d  9274  lemulge11d  9275  lemulge12d  9276  ltmul12ad  9279  lemul12ad  9280  lemul12bd  9281  nndivtr  9355  qreccl  10058  ledivdivd  10140  lediv12ad  10174  lt2mul2divd  10183  xlt2add  10299  xleaddadd  10306  iccss2  10363  iccssico2  10366  lincmb01cmp  10422  iccf1o  10424  fzrev2i  10510  qtri3or  10692  elicore  10718  2tnp1ge0ge0  10757  modqid  10807  q0mod  10813  q1mod  10814  modqabs  10815  modqadd1  10819  mulqaddmodid  10822  mulp1mod1  10823  modqmuladd  10824  modqmuladdnn0  10826  qnegmod  10827  m1modnnsub1  10828  addmodid  10830  modqm1p1mod0  10833  modqltm1p1mod  10834  modqmul1  10835  q2submod  10843  modifeq2int  10844  modaddmodup  10845  modaddmodlo  10846  modqaddmulmod  10849  modqsubdir  10851  modqeqmodmin  10852  modsumfzodifsn  10854  addmodlteq  10856  frecfzennn  10884  ser3mono  10945  expcl2lemap  11009  mulexpzap  11037  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  ltexp2a  11049  leexp2a  11050  sqdivap  11061  qsqeqor  11108  expnbnd  11122  expsubapd  11143  lt2sqd  11163  le2sqd  11164  sq11d  11165  apexp1  11178  bcp1nk  11222  hashunlem  11266  hashf1lem1  11307  zfz1isolem1  11314  hashtpgim  11319  sq01  11682  cjap  11694  cnreim  11766  resqrexlem1arp  11793  resqrexlemp1rp  11794  resqrexlemglsq  11810  abs00ap  11850  absext  11851  absexpzap  11869  absrele  11872  sqrtmuld  11958  sqrtsq2d  11959  sqrtled  11960  sqrtltd  11961  sqr11d  11962  abs3lemd  11990  minmax  12020  xrmaxiflemlub  12039  xrltmaxsup  12048  xrminmax  12056  xrbdtri  12067  climuni  12084  2clim  12092  addcn2  12101  mulcn2  12103  fsum3  12179  mptfzshft  12234  fsumrev  12235  fisum0diag2  12239  modfsummodlemstep  12249  binomlem  12275  mertenslemi1  12327  fprodrev  12411  efcllemp  12450  p1modz1  12586  dvds1  12645  dvdsext  12647  mulmoddvds  12655  oexpneg  12669  evennn02n  12674  evennn2n  12675  bitsinv1  12754  bezoutlemmo  12808  mulgcd  12818  dvdssqlem  12832  rpmulgcd2  12898  isprm6  12951  sqrt2irraplemnn  12984  sqrt2irrap  12985  sqrtrirr  13014  crth  13031  eulerthlemh  13038  prmdiveq  13043  powm2modprm  13060  modprm0  13062  pythagtriplem2  13074  pythagtriplem11  13082  pythagtriplem13  13084  pythagtrip  13091  pcid  13132  pcgcd1  13136  pcprmpw2  13141  dvdsprmpweqle  13145  pcaddlem  13147  pcadd  13148  fldivp1  13156  4sqlem12  13210  4sqlem14  13212  4sqlem15  13213  4sqlem16  13214  ballotfilemsima  13317  ballotfilemfrceq  13330  unennn  13346  ennnfonelemg  13352  ennnfonelemhf1o  13362  inffinp1  13378  isstructr  13425  setscomd  13451  imasbas  13687  imasplusg  13688  imasmulr  13689  subm0  13848  gzsumshift  14239  gsump1  14247  lssvancl1  14813  lssvnegcl  14822  lspprvacl  14859  lspsneli  14861  lspsn  14862  znf1o  15095  ntrin  15350  topssnei  15388  restbasg  15394  cnntri  15450  txcn  15501  txlm  15505  cnmpt2res  15523  psmetlecl  15560  xmetlecl  15593  bldisj  15627  bdmet  15728  bdbl  15729  bdmopn  15730  xmetxp  15733  metcnp  15738  tgioo  15780  cncfmet  15818  dedekindeulemlub  15846  suplociccreex  15850  ellimc3apf  15886  limcimolemlt  15890  limccnp2cntop  15903  dvfvalap  15907  dvidsslem  15919  dvmulxxbr  15928  dvaddxx  15929  dvmulxx  15930  dviaddf  15931  dvimulf  15932  dvcoapbr  15933  dvmptclx  15944  rpcxpmul2z  16148  cxplt3  16155  cxpltd  16163  cxpled  16164  cxplt3d  16170  cxple3d  16171  logbrec  16196  logbgcd1irraplemap  16205  zprmlogbaplem1  16215  log2tlbndlog2  16220  birthdaylem3  16227  pellexlem1  16229  pellexlem2  16230  wilthlem1  16232  ppiqsval  16240  chtqwordi  16263  ppiqwordi  16268  mpodvdsmulf1o  16284  ppiqub  16293  bclbnd  16307  bposlem7  16317  lgslem1  16324  lgslem3  16326  lgsdirprm  16358  gausslemma2dlem1f1o  16384  gausslemma2dlem6  16391  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem4  16397  lgseisen  16398  lgsquadlem1  16401  lgsquad2lem1  16405  lgsquad3  16408  m1lgs  16409  2lgslem1a1  16410  2sqlem7  16445  usgredg2v  16670  vtxd0nedgbfi  16745  clwwlknonex2  16885