MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl22anc Unicode version

Theorem syl22anc 1185
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
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 519 . 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 )
73, 4, 5, 6syl12anc 1182 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  fr2nr  4520  fr3nr  4719  soltmin  5232  f1oprg  5677  fveqf1o  5988  weniso  6034  smogt  6588  smorndom  6589  oacomf1o  6767  th3qlem1  6969  difsnen  7149  undom  7155  domss2  7225  ssenen  7240  marypha1lem  7396  fisupcl  7428  ordtypelem3  7445  ordtypelem8  7450  oieu  7464  oismo  7465  wofib  7470  wemaplem2  7472  wemapso  7476  wemapso2  7477  unxpwdom2  7512  infdifsn  7567  cantnf  7605  cnfcom3  7617  r1ordg  7660  dif1card  7848  infxpenlem  7851  dfac8clem  7869  infxp  8051  infmap2  8054  cflim2  8099  coftr  8109  fin2i2  8154  enfin2i  8157  fin23lem26  8161  fin23lem27  8164  fin23lem40  8187  isf32lem2  8190  isf32lem3  8191  isf32lem4  8192  isf32lem7  8195  isf32lem9  8197  fin1a2lem13  8248  fin12  8249  alephexp1  8410  gchdomtri  8460  fpwwe2lem12  8472  fpwwe2lem13  8473  gchhar  8502  gchpwdom  8505  adderpqlem  8787  mulerpqlem  8788  addassnq  8791  mulassnq  8792  distrnq  8794  mulidnq  8796  recmulnq  8797  ltexnq  8808  distrlem1pr  8858  distrlem4pr  8859  prlem936  8880  reclem3pr  8882  mulgt0d  9181  mul4d  9234  add4d  9245  add42d  9246  subcan  9312  addsub4d  9414  subadd4d  9415  sub4d  9416  2addsubd  9417  addsubeq4d  9418  muladdd  9447  mulsubd  9448  addgegt0d  9556  addge0d  9558  mulge0d  9559  le2addd  9600  le2subd  9601  ltleaddd  9602  leltaddd  9603  lt2subd  9605  divdivdiv  9671  divcan5  9672  divne0d  9762  recdivd  9763  recdiv2d  9764  divcan6d  9765  ddcand  9766  rec11d  9767  divmuldivd  9787  divmul13d  9788  divmul24d  9789  divadddivd  9790  divsubdivd  9791  divmuleqd  9792  divdivdivd  9793  subrecd  9801  recreclt  9865  divgt0d  9902  mulgt1d  9903  lemulge11d  9904  lemulge12d  9905  ltmul12ad  9908  lemul12ad  9909  lemul12bd  9910  supmul1  9929  nndivtr  9997  qreccl  10550  ledivdivd  10629  lediv12ad  10659  lt2mul2divd  10662  xlt2add  10795  supxrun  10850  supxrre  10862  infmxrre  10870  iccss2  10937  iccssico2  10940  lincmb01cmp  10994  iccf1o  10995  fzrev2i  11066  modsubdir  11240  fzennn  11262  sermono  11310  mulexpz  11375  expaddz  11379  ltexp2a  11386  leexp2a  11390  sqdiv  11402  expmulnbnd  11466  digit1  11468  expsubd  11489  lt2sqd  11512  le2sqd  11513  sq11d  11514  bcm1k  11561  bcp1n  11562  bcp1nk  11563  hashf1lem1  11659  absrele  12068  sqreulem  12118  sqrmuld  12182  sqrsq2d  12183  sqrled  12184  sqrltd  12185  sqr11d  12186  abs3lemd  12218  rlimuni  12299  climuni  12301  lo1resb  12313  o1resb  12315  2clim  12321  addcn2  12342  mulcn2  12344  o1of2  12361  o1rlimmul  12367  lo1add  12375  lo1mul  12376  isercolllem1  12413  caucvgrlem  12421  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  fsumrev  12517  fsumshft  12518  fsum0diag2  12521  binomlem  12563  climcndslem1  12584  climcndslem2  12585  harmonic  12593  mertenslem1  12616  efcllem  12635  moddvds  12814  dvds1  12853  dvdsext  12855  oexpneg  12866  bitsinv1  12909  sadaddlem  12933  sadasslem  12937  sadeq  12939  mulgcd  13001  dvdssqlem  13014  rpmulgcd2  13060  isprm6  13064  isprm5  13067  crt  13122  eulerthlem2  13126  prmdiveq  13130  pythagtriplem11  13154  pythagtriplem13  13156  iserodd  13164  pcgcd1  13205  pcprmpw2  13210  pcaddlem  13212  fldivp1  13221  4sqlem12  13279  4sqlem14  13281  4sqlem15  13282  4sqlem16  13283  vdwapun  13297  mreexexlem4d  13827  acsfn1  13841  acsfn2  13843  sscpwex  13970  rescabs  13988  catciso  14217  yonedainv  14333  p0le  14427  ple1  14428  subm0  14711  odmodnn0  15133  odeq  15143  dfod2  15155  sylow1lem1  15187  lsmsubg  15243  lsmmod  15262  lsmdisj2  15269  ghmplusg  15416  odadd  15420  gexexlem  15422  lt6abl  15459  cyggex2  15461  ablfacrp  15579  ablfacrp2  15580  ablfac1c  15584  ablfac1eu  15586  lssvancl1  15976  lssvnegcl  15987  lspprvacl  16030  lspsneli  16032  lspsn  16033  lmhmplusg  16075  lmhmima  16078  lmhmpreima  16079  reslmhm  16083  lbsind2  16108  lsmcl  16110  lsmelval2  16112  lsppreli  16117  lspprabs  16122  pj1lmhm  16127  lssvs0or  16137  lspabs3  16148  lspfixed  16155  lspexch  16156  lsmcv  16168  lspsolv  16170  lidlmcl  16243  drngnidl  16255  2idlcpbl  16260  mplbas2  16486  coe1addfv  16613  gzrngunit  16719  zlpirlem3  16725  prmirredlem  16728  znf1o  16787  znunithash  16800  ntrin  17080  topssnei  17143  restbas  17176  restntr  17200  cnntri  17289  fiuncmp  17421  nllyrest  17502  nllyidm  17505  hausllycmp  17510  cldllycmp  17511  hauspwdom  17517  txcld  17588  txcn  17611  txlly  17621  txnlly  17622  txhaus  17632  txlm  17633  txkgen  17637  xkococnlem  17644  cnmpt2res  17662  xkoinjcn  17672  basqtop  17696  qtopeu  17701  qtophmeo  17802  trfbas2  17828  neifil  17865  hausflim  17966  alexsubALTlem2  18032  cnextfval  18046  cnextfvval  18049  cnextf  18050  clssubg  18091  utop2nei  18233  utop3cls  18234  utopreg  18235  psmetlecl  18299  xmetlecl  18329  prdsxmetlem  18351  bldisj  18381  imasf1obl  18471  prdsbl  18474  stdbdmet  18499  stdbdmopn  18501  met2ndci  18505  metcnp  18524  metusttoOLD  18540  metustto  18541  metustexhalfOLD  18546  metustexhalf  18547  cfilucfilOLD  18552  cfilucfil  18553  metucnOLD  18571  metucn  18572  lssnlm  18689  nmotri  18726  nmoid  18729  tgioo  18780  blcvx  18782  xrsmopn  18796  reperflem  18802  reconnlem2  18811  opnreen  18815  metdsge  18832  metdsre  18836  metdscnlem  18838  metnrmlem1a  18841  metnrmlem1  18842  metnrmlem3  18844  cncfmet  18891  cnmpt2pc  18906  icopnfcnv  18920  icopnfhmeo  18921  cnllycmp  18934  evth  18937  lebnumii  18944  nmoleub2lem3  19076  iscfil2  19172  cfil3i  19175  iscfil3  19179  cfilfcls  19180  iscau3  19184  iscmet3lem2  19198  caubl  19213  lmcau  19218  minveclem2  19280  pjthlem1  19291  pjthlem2  19292  ivthicc  19308  ovollecl  19332  ovolunlem1a  19345  ovolunnul  19349  ovoliunlem1  19351  ismbl2  19376  nulmbl2  19384  unmbl  19385  volun  19392  voliunlem2  19398  ioombl1lem2  19406  uniioombllem2a  19427  uniioombllem3  19430  uniioombllem4  19431  dyaddisjlem  19440  dyadmaxlem  19442  opnmbllem  19446  volsup2  19450  volcn  19451  ismbfd  19485  mbfi1fseqlem1  19560  mbfi1fseqlem5  19564  itg2lecl  19583  itg2monolem2  19596  itg2gt0  19605  itgspliticc  19681  ellimc3  19719  limcres  19726  dvfval  19737  dvres3  19753  dvres3a  19754  dvnff  19762  dvnadd  19768  dvn2bss  19769  dvnres  19770  dvcmul  19783  dvcmulf  19784  dvmptres3  19795  dvmptres2  19801  dvmptntr  19810  dvexp3  19815  dvferm1lem  19821  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  dvgt0lem1  19839  dvgt0lem2  19840  dvne0  19848  lhop1lem  19850  lhop2  19852  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcvx  19857  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  ftc1lem6  19878  ftc1  19879  ftc2ditglem  19882  itgsubstlem  19885  evlslem3  19888  evlslem1  19889  evl1addd  19907  evl1subd  19908  evl1muld  19909  mdegaddle  19950  mdegmullem  19954  ply1rem  20039  fta1glem2  20042  fta1blem  20044  ig1peu  20047  ig1pdvds  20052  dgrmulc  20142  dgrcolem1  20144  plydivlem4  20166  plydiveu  20168  fta1lem  20177  vieta1lem1  20180  vieta1lem2  20181  plyexmo  20183  taylfvallem1  20226  taylfval  20228  tayl0  20231  taylplem1  20232  taylply2  20237  taylply  20238  dvtaylp  20239  dvntaylp  20240  dvntaylp0  20241  taylthlem1  20242  taylthlem2  20243  ulmcaulem  20263  ulmcau  20264  ulmcn  20268  ulmdvlem1  20269  radcnvlem1  20282  radcnvle  20289  psercn  20295  pserdvlem2  20297  pserdv  20298  abelth  20310  cosordlem  20386  tanregt0  20394  dvlog2lem  20496  efopn  20502  logtayllem  20503  logccv  20507  cxplt3  20544  cxpmul2zd  20560  cxpltd  20563  cxpled  20564  cxplt3d  20576  cxple3d  20577  dvsqr  20581  cxpcn3  20585  cxpaddle  20589  cxpeq  20594  angcan  20597  angvald  20599  ang180lem2  20605  ang180  20609  isosctrlem3  20617  dquartlem1  20644  atantayl2  20731  leibpilem1  20733  leibpi  20735  log2tlbnd  20738  birthdaylem3  20745  xrlimcnp  20760  efrlim  20761  o1cxp  20766  jensenlem2  20779  jensen  20780  fsumharmonic  20803  wilthlem1  20804  basellem3  20818  basellem6  20821  basellem8  20823  ppisval  20839  chtwordi  20892  ppiwordi  20898  mumullem2  20916  dvdsmulf1o  20932  fsumvma  20950  fsumvma2  20951  chpchtsum  20956  chpub  20957  logfacubnd  20958  dchrmulcl  20986  dchrinv  20998  dchrptlem1  21001  dchrptlem2  21002  sumdchr2  21007  dchr2sum  21010  bposlem7  21027  lgslem1  21033  lgslem3  21035  lgsdirprm  21066  lgsqrlem2  21079  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem4  21089  lgseisen  21090  lgsquadlem1  21091  lgsquad2lem1  21095  lgsquad3  21098  m1lgs  21099  2sqlem7  21107  chebbnd1lem2  21117  chebbnd1lem3  21118  rplogsumlem1  21131  rpvmasumlem  21134  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrvmasumlema  21147  dchrisum0flblem2  21156  dchrisum0fno1  21158  dchrisum0re  21160  logdivsum  21180  pntrsumbnd2  21214  pntpbnd1a  21232  pntpbnd1  21233  pntibndlem2  21238  pntlemr  21249  pntlemj  21250  pntlemf  21252  pnt2  21260  padicabv  21277  ostth2lem2  21281  usgraidx2v  21365  iseupa  21640  eupap1  21651  eupath2lem3  21654  nmobndi  22229  ubthlem2  22326  ubthlem3  22327  minvecolem2  22330  shuni  22755  pjhthlem1  22846  chscllem2  23093  pjcompi  23127  mayete3i  23183  mayete3iOLD  23184  unoplin  23376  hmoplin  23398  nmophmi  23487  mdslmd4i  23789  preqsnd  23953  isoun  24042  xrofsup  24079  eliccelico  24093  elicoelioo  24094  difioo  24098  rexdiv  24125  xrge0addgt0  24167  ofldchr  24197  unitdivcld  24252  xrge0mulc1cn  24280  qqhnm  24327  esumcst  24408  esumfsup  24413  esumpmono  24422  esumcvg  24429  difelsiga  24469  1stmbfm  24563  2ndmbfm  24564  dya2icoseg  24580  probmeasb  24641  orvcgteel  24678  orvclteel  24683  ballotlemsima  24726  ballotlemfrceq  24739  lgamucov  24775  lgamcvg2  24792  subfacp1lem2a  24819  subfaclim  24827  erdsze2lem2  24843  cvmliftlem2  24926  cvmliftlem10  24934  cvmliftlem13  24936  cvmliftiota  24941  cvmlift2lem9  24951  cvmlift2lem11  24953  cvmlift2lem12  24954  cvmliftphtlem  24957  cvmlift3lem6  24964  cvmlift3lem7  24965  cvmlift3lem9  24967  snmlff  24969  mulge0b  25144  fprodser  25228  fprodshft  25253  fprodrev  25254  rprisefaccl  25291  trpredelss  25449  trpredpo  25452  nodenselem5  25553  nobndlem6  25565  brbtwn2  25748  colinearalglem2  25750  axcgrtr  25758  axcgrid  25759  axsegconlem7  25766  axsegcon  25770  ax5seglem3  25774  ax5seglem6  25777  ax5seg  25781  axpaschlem  25783  axlowdimlem17  25801  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  brsegle  25946  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem  26155  itg2addnc  26158  itg2gt0cn  26159  ftc1cnnclem  26177  ftc1cnnc  26178  areacirclem6  26186  opnregcld  26223  indexdom  26326  sstotbnd2  26373  isbnd3  26383  isbnd3b  26384  cntotbnd  26395  ismtyima  26402  heibor1lem  26408  heiborlem8  26417  rrncmslem  26431  reheibor  26438  lcomfsup  26637  mzpsubst  26695  eldioph2lem1  26708  eldioph2lem2  26709  eldioph2b  26711  diophin  26721  irrapxlem2  26776  irrapxlem4  26778  irrapxlem5  26779  pellexlem1  26782  pellexlem2  26783  pellexlem6  26787  elpell1qr2  26825  pell1qrgaplem  26826  pell1qrgap  26827  pellqrex  26832  pellfundex  26839  pellfund14  26851  rmspecsqrnq  26859  rmxyadd  26874  expmordi  26900  rmxypos  26902  jm2.24  26918  congsub  26925  mzpcong  26927  congrep  26928  acongtr  26933  acongrep  26935  jm2.19lem1  26950  jm2.22  26956  jm2.23  26957  jm2.26lem3  26962  jm2.26  26963  jm2.27a  26966  fnwe2lem2  27016  aomclem6  27024  frlmvscaval  27099  frlmssuvc1  27114  frlmsslsp  27116  frlmup1  27118  frlmup2  27119  enfixsn  27125  lindfind2  27156  lindfrn  27159  f1lindf  27160  islindf4  27176  hbtlem2  27196  hbtlem4  27198  hbtlem5  27200  dgraa0p  27222  rngunsnply  27246  pmtrff1o  27272  pmtrfcnv  27273  pmtrfb  27274  psgnunilem1  27284  mamudi  27329  mamudir  27330  acsfn1p  27375  proot1hash  27387  expgrowth  27420  itgsinexplem1  27615  stoweidlem11  27627  stoweidlem26  27642  stoweidlem34  27650  stoweidlem36  27652  stoweidlem38  27654  stirlinglem5  27694  lkrlsp  29585  lshpkrlem5  29597  ldualssvscl  29641  ldualssvsubcl  29642  llnmlplnN  30021  llncvrlpln  30040  pmapjat1  30335  pclfinN  30382  lautlt  30573  lauteq  30577  lautco  30579  ltrn11  30608  ltrnle  30611  ltrneq2  30630  cdlemednuN  30782  cdleme20k  30801  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme21c  30809  cdleme22e  30826  cdleme22eALTN  30827  cdlemefrs32fva  30882  cdlemg4g  31098  cdlemg18b  31161  cdlemg18c  31162  cdlemj3  31305  dia2dimlem5  31551  dvhopN  31599  cdlemm10N  31601  dihjatcclem4  31904  dochexmidlem2  31944  lclkrlem2o  32004  lcfrlem5  32029  lcfrlem6  32030  lcdlssvscl  32089  mapdpglem6  32161  mapdpglem9  32163  mapdpglem12  32166  mapdpglem14  32168  mapdindp0  32202  hdmaprnlem7N  32341  hdmaprnlem8N  32342  hdmaprnlem3eN  32344  hgmapvvlem3  32411
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator