Theorem syl22anc 1275

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 1272	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  5665  tfrexlem  6578  th3qlem1  6884  en2prd  7072  enpr2d  7077  ssenen  7118  phplem4dom  7129  phplem4on  7135  fiunsnnn  7151  findcard2sd  7162  unsnfi  7192  sbthlemi9  7248  fsuppcorn  7267  endjusym  7400  endjudisj  7530  djuen  7531  ltanqg  7731  ltmnqg  7732  ltnnnq  7754  addcmpblnq0  7774  addlocprlemeqgt  7863  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  addcanprleml  7945  recexprlem1ssl  7964  caucvgprlemloc  8006  caucvgprprlemloccalc  8015  mulcmpblnr  8072  ltasrg  8101  recexgt0sr  8104  mulextsr1lem  8111  mulextsr1  8112  srpospr  8114  prsrlt  8118  ltpsrprg  8134  mappsrprg  8135  pitonnlem1p1  8177  recidpirq  8189  axpre-ltadd  8217  mulgt0d  8412  mul4d  8444  add4d  8458  add42d  8459  subcan  8544  addsub4d  8647  subadd4d  8648  sub4d  8649  2addsubd  8650  addsubeq4d  8651  muladdd  8706  mulsubd  8707  addgegt0d  8810  addgtge0d  8811  addge0d  8813  le2addd  8854  le2subd  8855  ltleaddd  8856  leltaddd  8857  lt2subd  8859  apreap  8878  apsym  8897  apcotr  8898  apadd1  8899  apneg  8902  mulext1  8903  mulap0r  8906  mulge0d  8912  mulap0d  8949  divdivdivap  9004  divcanap5  9005  divap0d  9097  recdivapd  9098  recdivap2d  9099  divcanap6d  9100  ddcanapd  9101  rec11apd  9102  divmuldivapd  9123  divmuleqapd  9124  subrecapd  9132  prodgt0  9143  lt2msq  9177  ledivdiv  9181  lediv12a  9185  recreclt  9191  divgt0d  9226  mulgt1d  9227  lemulge11d  9228  lemulge12d  9229  ltmul12ad  9232  lemul12ad  9233  lemul12bd  9234  nndivtr  9296  qreccl  9992  ledivdivd  10073  lediv12ad  10107  lt2mul2divd  10116  xlt2add  10232  xleaddadd  10239  iccss2  10296  iccssico2  10299  lincmb01cmp  10355  iccf1o  10357  fzrev2i  10442  qtri3or  10624  elicore  10650  2tnp1ge0ge0  10685  modqid  10735  q0mod  10741  q1mod  10742  modqabs  10743  modqadd1  10747  mulqaddmodid  10750  mulp1mod1  10751  modqmuladd  10752  modqmuladdnn0  10754  qnegmod  10755  m1modnnsub1  10756  addmodid  10758  modqm1p1mod0  10761  modqltm1p1mod  10762  modqmul1  10763  q2submod  10771  modifeq2int  10772  modaddmodup  10773  modaddmodlo  10774  modqaddmulmod  10777  modqsubdir  10779  modqeqmodmin  10780  modsumfzodifsn  10782  addmodlteq  10784  frecfzennn  10812  ser3mono  10873  expcl2lemap  10937  mulexpzap  10965  expaddzaplem  10968  expaddzap  10969  expmulzap  10971  ltexp2a  10977  leexp2a  10978  sqdivap  10989  qsqeqor  11036  expnbnd  11050  expsubapd  11071  lt2sqd  11091  le2sqd  11092  sq11d  11093  apexp1  11105  bcp1nk  11149  hashunlem  11193  zfz1isolem1  11237  hashtpgim  11242  cjap  11616  cnreim  11688  resqrexlem1arp  11715  resqrexlemp1rp  11716  resqrexlemglsq  11732  abs00ap  11772  absext  11773  absexpzap  11790  absrele  11793  sqrtmuld  11879  sqrtsq2d  11880  sqrtled  11881  sqrtltd  11882  sqr11d  11883  abs3lemd  11911  minmax  11940  xrmaxiflemlub  11958  xrltmaxsup  11967  xrminmax  11975  xrbdtri  11986  climuni  12003  2clim  12011  addcn2  12020  mulcn2  12022  fsum3  12098  mptfzshft  12153  fsumrev  12154  fisum0diag2  12158  modfsummodlemstep  12168  binomlem  12194  mertenslemi1  12246  fprodrev  12330  efcllemp  12369  p1modz1  12505  dvds1  12564  dvdsext  12566  mulmoddvds  12574  oexpneg  12588  evennn02n  12593  evennn2n  12594  bitsinv1  12673  bezoutlemmo  12727  mulgcd  12737  dvdssqlem  12751  rpmulgcd2  12817  isprm6  12869  sqrt2irraplemnn  12901  sqrt2irrap  12902  crth  12946  eulerthlemh  12953  prmdiveq  12958  powm2modprm  12975  modprm0  12977  pythagtriplem2  12989  pythagtriplem11  12997  pythagtriplem13  12999  pythagtrip  13006  pcid  13047  pcgcd1  13051  pcprmpw2  13056  dvdsprmpweqle  13060  pcaddlem  13062  pcadd  13063  fldivp1  13071  4sqlem12  13125  4sqlem14  13127  4sqlem15  13128  4sqlem16  13129  ballotfilemsima  13203  ballotfilemfrceq  13216  unennn  13232  ennnfonelemg  13238  ennnfonelemhf1o  13248  inffinp1  13264  isstructr  13311  setscomd  13337  imasbas  13571  imasplusg  13572  imasmulr  13573  subm0  13737  gsumshift  14105  gfsump1  14108  lssvancl1  14641  lssvnegcl  14650  lspprvacl  14687  lspsneli  14689  lspsn  14690  znf1o  14925  ntrin  15115  topssnei  15153  restbasg  15159  cnntri  15215  txcn  15266  txlm  15270  cnmpt2res  15288  psmetlecl  15325  xmetlecl  15358  bldisj  15392  bdmet  15493  bdbl  15494  bdmopn  15495  xmetxp  15498  metcnp  15503  tgioo  15545  cncfmet  15583  dedekindeulemlub  15611  suplociccreex  15615  ellimc3apf  15651  limcimolemlt  15655  limccnp2cntop  15668  dvfvalap  15672  dvidsslem  15684  dvmulxxbr  15693  dvaddxx  15694  dvmulxx  15695  dviaddf  15696  dvimulf  15697  dvcoapbr  15698  dvmptclx  15709  cxplt3  15911  cxpltd  15919  cxpled  15920  cxplt3d  15926  cxple3d  15927  logbrec  15951  logbgcd1irraplemap  15960  pellexlem1  15971  pellexlem2  15972  wilthlem1  15974  mpodvdsmulf1o  15984  lgslem1  15999  lgslem3  16001  lgsdirprm  16033  gausslemma2dlem1f1o  16059  gausslemma2dlem6  16066  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem4  16072  lgseisen  16073  lgsquadlem1  16076  lgsquad2lem1  16080  lgsquad3  16083  m1lgs  16084  2lgslem1a1  16085  2sqlem7  16120  usgredg2v  16345  vtxd0nedgbfi  16420  clwwlknonex2  16560