Theorem syl22anc 1327

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.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		syl12anc.1	. . 3 |- ( ph -> ps )
2		syl12anc.2	. . 3 |- ( ph -> ch )
3	1, 2	jca 554	. 2 |- ( ph -> ( ps /\ ch ) )
4		syl12anc.3	. 2 |- ( ph -> th )
5		syl22anc.4	. 2 |- ( ph -> ta )
6		syl22anc.5	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) ) -> et )
7	3, 4, 5, 6	syl12anc 1324	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  preqsnd  4392  fr2nr  5092  soltmin  5532  f1oprg  6181  f1prex  6539  fveqf1o  6557  weniso  6604  fr3nr  6979  smogt  7464  smorndom  7465  oacomf1o  7645  difsnen  8042  undom  8048  enfixsn  8069  domss2  8119  ssenen  8134  marypha1lem  8339  fisupcl  8375  ordtypelem3  8425  ordtypelem8  8430  oieu  8444  oismo  8445  wofib  8450  wemaplem2  8452  wemapso  8456  wemapso2lem  8457  unxpwdom2  8493  infdifsn  8554  oemapvali  8581  cantnflem1c  8584  cantnflem1  8586  cantnf  8590  cnfcom3  8601  r1ordg  8641  dif1card  8833  infxpenlem  8836  dfac8clem  8855  infxp  9037  infmap2  9040  cflim2  9085  coftr  9095  fin2i2  9140  enfin2i  9143  fin23lem26  9147  fin23lem27  9150  fin23lem40  9173  isf32lem2  9176  isf32lem3  9177  isf32lem4  9178  isf32lem7  9181  isf32lem9  9183  fin1a2lem13  9234  fin12  9235  alephexp1  9401  gchdomtri  9451  fpwwe2lem12  9463  fpwwe2lem13  9464  gchpwdom  9492  gchhar  9501  adderpqlem  9776  mulerpqlem  9777  addassnq  9780  mulassnq  9781  distrnq  9783  mulidnq  9785  recmulnq  9786  ltexnq  9797  distrlem1pr  9847  distrlem4pr  9848  prlem936  9869  reclem3pr  9871  mulcmpblnr  9892  mulgt0d  10192  mul4d  10248  add4d  10264  add42d  10265  subcan  10336  addsub4d  10439  subadd4d  10440  sub4d  10441  2addsubd  10442  addsubeq4d  10443  muladdd  10489  mulsubd  10490  addgegt0d  10601  addge0d  10603  mulge0d  10604  le2addd  10646  le2subd  10647  ltleaddd  10648  leltaddd  10649  lt2subd  10651  divdivdiv  10726  divcan5  10727  divne0d  10817  recdivd  10818  recdiv2d  10819  divcan6d  10820  ddcand  10821  rec11d  10822  divmuldivd  10842  divmul13d  10843  divmul24d  10844  divadddivd  10845  divsubdivd  10846  divmuleqd  10847  divdivdivd  10848  subrecd  10856  mulge0b  10893  recreclt  10922  divgt0d  10959  mulgt1d  10960  lemulge11d  10961  lemulge12d  10962  ltmul12ad  10965  lemul12ad  10966  lemul12bd  10967  supmul1  10992  nndivtr  11062  qreccl  11808  ledivdivd  11897  lediv12ad  11931  lt2mul2divd  11939  xlt2add  12090  supxrun  12146  supxrre  12157  infxrre  12166  elicore  12226  iccss2  12244  iccssico2  12247  lincmb01cmp  12315  iccf1o  12316  fzrev2i  12405  fz1fzo0m1  12515  2tnp1ge0ge0  12630  m1modnnsub1  12716  modaddmodup  12733  modaddmodlo  12734  modsubdir  12739  fzennn  12767  sermono  12833  mulexpz  12900  expaddz  12904  ltexp2a  12912  leexp2a  12916  sqdiv  12928  expmulnbnd  12996  digit1  12998  expsubd  13019  lt2sqd  13043  le2sqd  13044  sq11d  13045  bcm1k  13102  bcp1n  13103  bcp1nk  13104  hashf1lem1  13239  cshw1  13568  2swrd2eqwrdeq  13696  ofccat  13708  absrele  14048  sqreulem  14099  sqrtmuld  14163  sqrtsq2d  14164  sqrtled  14165  sqrtltd  14166  sqr11d  14167  abs3lemd  14200  rlimuni  14281  climuni  14283  lo1resb  14295  o1resb  14297  2clim  14303  addcn2  14324  mulcn2  14326  o1of2  14343  o1rlimmul  14349  lo1add  14357  lo1mul  14358  isercolllem1  14395  caucvgrlem  14403  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  mptfzshft  14510  fsumrev  14511  fsum0diag2  14515  binomlem  14561  climcndslem1  14581  climcndslem2  14582  harmonic  14591  mertenslem1  14616  fprodser  14679  fprodrev  14707  rprisefaccl  14754  efcllem  14808  moddvds  14991  dvds1  15041  dvdsext  15043  oexpneg  15069  evennn02n  15074  evennn2n  15075  bitsinv1  15164  sadaddlem  15188  sadasslem  15192  sadeq  15194  mulgcd  15265  dvdssqlem  15279  lcmftp  15349  rpmulgcd2  15370  coprmproddvdslem  15376  isprm5  15419  isprm6  15426  crth  15483  eulerthlem2  15487  prmdiveq  15491  pythagtriplem11  15530  pythagtriplem13  15532  iserodd  15540  pcgcd1  15581  pcprmpw2  15586  pcaddlem  15592  fldivp1  15601  4sqlem12  15660  4sqlem14  15662  4sqlem15  15663  4sqlem16  15664  vdwapun  15678  mreexexlem4d  16307  acsfn1  16322  acsfn2  16324  sscpwex  16475  rescabs  16493  yonedainv  16921  subm0  17356  pmtrfb  17885  psgnunilem1  17913  odmodnn0  17959  odeq  17969  dfod2  17981  sylow1lem1  18013  lsmsubg  18069  lsmmod  18088  lsmdisj2  18095  ghmplusg  18249  odadd  18253  gexexlem  18255  lt6abl  18296  cyggex2  18298  dprdfinv  18418  dmdprdsplitlem  18436  dpjidcl  18457  ablfacrp  18465  ablfacrp2  18466  ablfac1c  18470  ablfac1eu  18472  lcomfsupp  18903  lssvancl1  18945  lssvnegcl  18956  lspprvacl  18999  lspsneli  19001  lspsn  19002  lmhmplusg  19044  lmhmima  19047  lmhmpreima  19048  reslmhm  19052  lbsind2  19081  lsmcl  19083  lsmelval2  19085  lsppreli  19090  lspprabs  19095  pj1lmhm  19100  lssvs0or  19110  lspabs3  19121  lspfixed  19128  lspexch  19129  lsmcv  19141  lspsolv  19143  lidlmcl  19217  drngnidl  19229  2idlcpbl  19234  mplbas2  19470  evlslem3  19514  evlslem1  19515  coe1addfv  19635  lply1binom  19676  evl1addd  19705  evl1subd  19706  evl1muld  19707  gzrngunit  19812  zringlpirlem3  19834  prmirredlem  19841  znf1o  19900  znunithash  19913  frlmsubgval  20108  frlmvscaval  20110  frlmphllem  20119  frlmphl  20120  frlmssuvc1  20133  frlmsslsp  20135  frlmup1  20137  frlmup2  20138  lindfind2  20157  lindfrn  20160  f1lindf  20161  islindf4  20177  mamudi  20209  mamudir  20210  1marepvmarrepid  20381  mdetrlin  20408  smadiadetglem1  20477  smadiadetg  20479  cramerimplem1  20489  mat2pmatscmxcl  20545  m2pmfzgsumcl  20553  pmatcollpw  20586  pmatcollpwfi  20587  pmatcollpw3fi1lem1  20591  cpmidpmatlem2  20676  cpmadugsumlemF  20681  chcoeffeqlem  20690  ntrin  20865  topssnei  20928  restbas  20962  restntr  20986  cnntri  21075  fiuncmp  21207  nllyrest  21289  nllyidm  21292  hausllycmp  21297  cldllycmp  21298  hauspwdom  21304  txcld  21406  txcn  21429  txlly  21439  txnlly  21440  txhaus  21450  txlm  21451  txkgen  21455  xkococnlem  21462  cnmpt2res  21480  xkoinjcn  21490  basqtop  21514  qtopeu  21519  trfbas2  21647  neifil  21684  hausflim  21785  alexsubALTlem2  21852  cnextfval  21866  cnextfvval  21869  cnextf  21870  cnextfres  21873  clssubg  21912  utop2nei  22054  utop3cls  22055  utopreg  22056  psmetlecl  22120  xmetlecl  22151  prdsxmetlem  22173  bldisj  22203  imasf1obl  22293  prdsbl  22296  stdbdmet  22321  stdbdmopn  22323  met2ndci  22327  metcnp  22346  metustto  22358  metustexhalf  22361  cfilucfil  22364  metucn  22376  lssnlm  22505  nmotri  22543  nmoid  22546  tgioo  22599  blcvx  22601  xrsmopn  22615  reperflem  22621  reconnlem2  22630  opnreen  22634  metdsge  22652  metdsre  22656  metdscnlem  22658  metnrmlem1a  22661  metnrmlem1  22662  metnrmlem3  22664  cncfmet  22711  cnmpt2pc  22727  icopnfcnv  22741  icopnfhmeo  22742  cnllycmp  22755  evth  22758  lebnumii  22765  nmoleub2lem3  22915  iscfil2  23064  cfil3i  23067  iscfil3  23071  cfilfcls  23072  iscau3  23076  iscmet3lem2  23090  caubl  23106  lmcau  23111  rrxcph  23180  minveclem2  23197  pjthlem1  23208  pjthlem2  23209  ivthicc  23227  ovollecl  23251  ovolunlem1a  23264  ovolunnul  23268  ovoliunlem1  23270  ismbl2  23295  nulmbl2  23304  unmbl  23305  volun  23313  voliunlem2  23319  ioombl1lem2  23327  uniioombllem2a  23350  uniioombllem3  23353  uniioombllem4  23354  dyaddisjlem  23363  dyadmaxlem  23365  opnmbllem  23369  volsup2  23373  volcn  23374  ismbfd  23407  mbfi1fseqlem1  23482  mbfi1fseqlem5  23486  itg2lecl  23505  itg2monolem2  23518  itg2gt0  23527  itgspliticc  23603  ellimc3  23643  limcres  23650  dvfval  23661  dvres3  23677  dvres3a  23678  dvnff  23686  dvnadd  23692  dvn2bss  23693  dvnres  23694  dvcmul  23707  dvcmulf  23708  dvmptres3  23719  dvmptres2  23725  dvmptntr  23734  dvexp3  23741  dvferm1lem  23747  dvlip  23756  dvlipcn  23757  dvlip2  23758  c1liplem1  23759  dvgt0lem1  23765  dvgt0lem2  23766  dvne0  23774  lhop1lem  23776  lhop2  23778  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcvx  23783  dvfsumle  23784  dvfsumabs  23786  dvfsumlem2  23790  ftc1lem6  23804  ftc1  23805  ftc2ditglem  23808  itgsubstlem  23811  tdeglem4  23820  mdegaddle  23834  mdegmullem  23838  ply1rem  23923  fta1glem2  23926  fta1blem  23928  ig1peu  23931  ig1pdvds  23936  dgrmulc  24027  dgrcolem1  24029  plydivlem4  24051  plydiveu  24053  fta1lem  24062  vieta1lem1  24065  vieta1lem2  24066  plyexmo  24068  taylfvallem1  24111  taylfval  24113  tayl0  24116  taylplem1  24117  taylply2  24122  taylply  24123  dvtaylp  24124  dvntaylp  24125  dvntaylp0  24126  taylthlem1  24127  taylthlem2  24128  ulmcaulem  24148  ulmcau  24149  ulmcn  24153  ulmdvlem1  24154  radcnvlem1  24167  radcnvle  24174  psercn  24180  pserdvlem2  24182  pserdv  24183  abelth  24195  cosordlem  24277  tanregt0  24285  dvlog2lem  24398  efopn  24404  logtayllem  24405  logccv  24409  cxplt3  24446  cxpmul2zd  24462  cxpltd  24465  cxpled  24466  cxplt3d  24478  cxple3d  24479  dvsqrt  24483  cxpcn3  24489  cxpaddle  24493  cxpeq  24498  angcan  24532  angvald  24534  ang180lem2  24540  ang180  24544  isosctrlem3  24550  dquartlem1  24578  atantayl2  24665  leibpilem1  24667  leibpi  24669  log2tlbnd  24672  birthdaylem3  24680  xrlimcnp  24695  efrlim  24696  o1cxp  24701  jensenlem2  24714  jensen  24715  fsumharmonic  24738  lgamucov  24764  lgamcvg2  24781  wilthlem1  24794  basellem3  24809  basellem6  24812  basellem8  24814  ppisval  24830  chtwordi  24882  ppiwordi  24888  mumullem2  24906  dvdsmulf1o  24920  fsumvma  24938  fsumvma2  24939  chpchtsum  24944  chpub  24945  logfacubnd  24946  dchrmulcl  24974  dchrinv  24986  dchrptlem1  24989  dchrptlem2  24990  sumdchr2  24995  dchr2sum  24998  bposlem7  25015  lgslem1  25022  lgslem3  25024  lgsdirprm  25056  lgsqrlem2  25072  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquad2lem1  25109  lgsquad3  25112  m1lgs  25113  2sqlem7  25149  chebbnd1lem2  25159  chebbnd1lem3  25160  rplogsumlem1  25173  rpvmasumlem  25176  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasumlema  25189  dchrisum0flblem2  25198  dchrisum0fno1  25200  dchrisum0re  25202  logdivsum  25222  pntrsumbnd2  25256  pntpbnd1a  25274  pntpbnd1  25275  pntibndlem2  25280  pntlemr  25291  pntlemj  25292  pntlemf  25294  pnt2  25302  padicabv  25319  ostth2lem2  25323  f1otrg  25751  brbtwn2  25785  colinearalglem2  25787  axcgrtr  25795  axcgrid  25796  axsegconlem7  25803  axsegcon  25807  ax5seglem3  25811  ax5seglem6  25814  ax5seg  25818  axpaschlem  25820  axlowdimlem17  25838  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  ecgrtg  25863  usgredg2v  26119  vtxdgoddnumeven  26449  2trlond  26835  eupthp1  27076  numclwwlkovf2ex  27219  nmobndi  27630  ubthlem2  27727  ubthlem3  27728  minvecolem2  27731  shuni  28159  pjhthlem1  28250  chscllem2  28497  pjcompi  28531  mayete3i  28587  unoplin  28779  hmoplin  28801  nmophmi  28890  mdslmd4i  29192  isoun  29479  xrge0addcld  29527  xrofsup  29533  eliccelico  29539  elicoelioo  29540  difioo  29544  rexdiv  29634  2sqmod  29648  xrge0addgt0  29691  omndadd2d  29708  omndadd2rd  29709  omndmul2  29712  ofldchr  29814  mdetpmtr2  29890  mdetpmtr12  29891  madjusmdetlem1  29893  madjusmdetlem4  29896  unitdivcld  29947  xrge0mulc1cn  29987  qqhnm  30034  esumcst  30125  esumfsup  30132  esumpmono  30141  esumcvg  30148  difelsiga  30196  sigapisys  30218  sigapildsys  30225  ldgenpisyslem1  30226  1stmbfm  30322  2ndmbfm  30323  dya2icoseg  30339  sibfinima  30401  probmeasb  30492  orvcgteel  30529  orvclteel  30534  ballotlemsima  30577  ballotlemfrceq  30590  sgnmul  30604  ccatmulgnn0dir  30619  fct2relem  30675  ftc2re  30676  chtvalz  30707  subfacp1lem2a  31162  subfaclim  31170  erdsze2lem2  31186  cvmliftlem2  31268  cvmliftlem10  31276  cvmliftlem13  31278  cvmliftiota  31283  cvmlift2lem9  31293  cvmlift2lem11  31295  cvmlift2lem12  31296  cvmliftphtlem  31299  cvmlift3lem6  31306  cvmlift3lem7  31307  cvmlift3lem9  31309  snmlff  31311  mrsubfval  31405  trpredelss  31732  trpredpo  31735  wzel  31771  wzelOLD  31772  wsuclem  31773  wsuclemOLD  31774  sltrec  31924  brsegle  32215  opnregcld  32325  addgtge0d  32496  fin2so  33396  poimirlem17  33426  poimirlem23  33432  opnmbllem0  33445  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem  33461  itg2addnc  33464  itg2gt0cn  33465  ftc1cnnclem  33483  ftc1cnnc  33484  areacirclem5  33504  indexdom  33529  sstotbnd2  33573  isbnd3  33583  isbnd3b  33584  cntotbnd  33595  ismtyima  33602  heibor1lem  33608  heiborlem8  33617  rrncmslem  33631  reheibor  33638  lkrlsp  34389  lshpkrlem5  34401  ldualssvscl  34445  ldualssvsubcl  34446  llnmlplnN  34825  llncvrlpln  34844  pmapjat1  35139  pclfinN  35186  lautlt  35377  lauteq  35381  lautco  35383  ltrn11  35412  ltrnle  35415  ltrneq2  35434  cdlemednuN  35587  cdleme20k  35607  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21c  35615  cdleme22e  35632  cdleme22eALTN  35633  cdlemefrs32fva  35688  cdlemg4g  35904  cdlemg18b  35967  cdlemg18c  35968  cdlemj3  36111  dia2dimlem5  36357  dvhopN  36405  cdlemm10N  36407  dihjatcclem4  36710  dochexmidlem2  36750  lclkrlem2o  36810  lcfrlem5  36835  lcfrlem6  36836  lcdlssvscl  36895  mapdpglem6  36967  mapdpglem9  36969  mapdpglem12  36972  mapdpglem14  36974  mapdindp0  37008  hdmaprnlem7N  37147  hdmaprnlem8N  37148  hdmaprnlem3eN  37150  hgmapvvlem3  37217  mzpsubst  37311  eldioph2lem1  37323  eldioph2lem2  37324  eldioph2b  37326  diophin  37336  irrapxlem2  37387  irrapxlem4  37389  irrapxlem5  37390  pellexlem1  37393  pellexlem2  37394  pellexlem6  37398  elpell1qr2  37436  pell1qrgaplem  37437  pell1qrgap  37438  pellqrex  37443  pellfundex  37450  pellfund14  37462  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  rmxyadd  37486  expmordi  37512  rmxypos  37514  jm2.24  37530  congsub  37537  mzpcong  37539  congrep  37540  acongtr  37545  acongrep  37547  jm2.19lem1  37556  jm2.22  37562  jm2.23  37563  jm2.26lem3  37568  jm2.26  37569  jm2.27a  37572  fnwe2lem2  37621  aomclem6  37629  hbtlem2  37694  hbtlem4  37696  hbtlem5  37698  dgraa0p  37719  rngunsnply  37743  acsfn1p  37769  proot1hash  37778  itgpowd  37800  expgrowth  38534  fpmd  39483  abslt2sqd  39576  ioondisj2  39714  ioondisj1  39715  eliocre  39734  ioossioobi  39743  iooiinicc  39769  iooiinioc  39783  icossico2  39791  lptioo2  39863  limcresiooub  39874  limsupequzlem  39954  xlimmnfvlem2  40059  xlimpnfvlem2  40063  cncfuni  40099  cncfiooicclem1  40106  cxpcncf2  40113  dvcnre  40130  dvresntr  40132  dvmptresicc  40134  dvresioo  40136  dvbdfbdioolem1  40143  dvnmptdivc  40153  dvnxpaek  40157  itgsinexplem1  40169  itgcoscmulx  40185  itgiccshift  40196  itgperiod  40197  ovolsplit  40205  stoweidlem11  40228  stoweidlem26  40243  stoweidlem34  40251  stoweidlem36  40253  stoweidlem38  40255  stirlinglem5  40295  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem20  40344  fourierdlem58  40381  fourierdlem72  40395  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem79  40402  fourierdlem80  40403  fourierdlem87  40410  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem113  40436  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem46  40497  etransclem47  40498  rrndistlt  40510  rrnprjdstle  40521  ioorrnopnxrlem  40526  sge0ssre  40614  sge0seq  40663  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmvlelem1  40809  hoidifhspdmvle  40834  hoiqssbllem2  40837  ovolval5lem2  40867  iinhoiicc  40888  iunhoiioo  40890  vonioolem2  40895  vonicclem2  40898  issmflem  40936  iccpartdisj  41373  m1expevenALTV  41560  oexpnegALTV  41588  tgoldbach  41705  tgoldbachOLD  41712  nn0eo  42322  fdivpm  42337  refdivpm  42338  elbigolo1  42351  logbpw2m1  42361  fllog2  42362  dignn0flhalflem1  42409  dignn0flhalflem2  42410