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

Theorem syl22anc 1184
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 518 . 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 1181 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  fr2nr  4474  fr3nr  4674  soltmin  5185  f1oprg  5622  fveqf1o  5929  weniso  5975  smogt  6526  smorndom  6527  oacomf1o  6705  th3qlem1  6907  difsnen  7087  undom  7093  domss2  7163  ssenen  7178  marypha1lem  7333  fisupcl  7365  ordtypelem3  7382  ordtypelem8  7387  oieu  7401  oismo  7402  wofib  7407  wemaplem2  7409  wemapso  7413  wemapso2  7414  unxpwdom2  7449  infdifsn  7504  cantnf  7542  cnfcom3  7554  r1ordg  7597  dif1card  7785  infxpenlem  7788  dfac8clem  7806  infxp  7988  infmap2  7991  cflim2  8036  coftr  8046  fin2i2  8091  enfin2i  8094  fin23lem26  8098  fin23lem27  8101  fin23lem40  8124  isf32lem2  8127  isf32lem3  8128  isf32lem4  8129  isf32lem7  8132  isf32lem9  8134  fin1a2lem13  8185  fin12  8186  alephexp1  8348  gchdomtri  8398  fpwwe2lem12  8410  fpwwe2lem13  8411  gchhar  8440  gchpwdom  8443  adderpqlem  8725  mulerpqlem  8726  addassnq  8729  mulassnq  8730  distrnq  8732  mulidnq  8734  recmulnq  8735  ltexnq  8746  distrlem1pr  8796  distrlem4pr  8797  prlem936  8818  reclem3pr  8820  mulgt0d  9118  mul4d  9171  add4d  9182  add42d  9183  subcan  9249  addsub4d  9351  subadd4d  9352  sub4d  9353  2addsubd  9354  addsubeq4d  9355  muladdd  9384  mulsubd  9385  addgegt0d  9493  addge0d  9495  mulge0d  9496  le2addd  9537  le2subd  9538  ltleaddd  9539  leltaddd  9540  lt2subd  9542  divdivdiv  9608  divcan5  9609  divne0d  9699  recdivd  9700  recdiv2d  9701  divcan6d  9702  ddcand  9703  rec11d  9704  divmuldivd  9724  divmul13d  9725  divmul24d  9726  divadddivd  9727  divsubdivd  9728  divmuleqd  9729  divdivdivd  9730  subrecd  9738  recreclt  9802  divgt0d  9839  mulgt1d  9840  lemulge11d  9841  lemulge12d  9842  ltmul12ad  9845  lemul12ad  9846  lemul12bd  9847  supmul1  9866  nndivtr  9934  qreccl  10487  ledivdivd  10566  lediv12ad  10596  lt2mul2divd  10599  xlt2add  10732  supxrun  10787  supxrre  10799  infmxrre  10807  iccss2  10873  iccssico2  10876  lincmb01cmp  10930  iccf1o  10931  fzrev2i  11001  modsubdir  11172  fzennn  11194  sermono  11242  mulexpz  11307  expaddz  11311  ltexp2a  11318  leexp2a  11322  sqdiv  11334  expmulnbnd  11398  digit1  11400  expsubd  11421  lt2sqd  11444  le2sqd  11445  sq11d  11446  bcm1k  11493  bcp1n  11494  bcp1nk  11495  hashf1lem1  11591  absrele  12000  sqreulem  12050  sqrmuld  12114  sqrsq2d  12115  sqrled  12116  sqrltd  12117  sqr11d  12118  abs3lemd  12150  rlimuni  12231  climuni  12233  lo1resb  12245  o1resb  12247  2clim  12253  addcn2  12274  mulcn2  12276  o1of2  12293  o1rlimmul  12299  lo1add  12307  lo1mul  12308  isercolllem1  12345  caucvgrlem  12353  iseraltlem2  12363  iseraltlem3  12364  iseralt  12365  fsumrev  12449  fsumshft  12450  fsum0diag2  12453  binomlem  12495  climcndslem1  12516  climcndslem2  12517  harmonic  12525  mertenslem1  12548  efcllem  12567  moddvds  12746  dvds1  12785  dvdsext  12787  oexpneg  12798  bitsinv1  12841  sadaddlem  12865  sadasslem  12869  sadeq  12871  mulgcd  12933  dvdssqlem  12946  rpmulgcd2  12992  isprm6  12996  isprm5  12999  crt  13054  eulerthlem2  13058  prmdiveq  13062  pythagtriplem11  13086  pythagtriplem13  13088  iserodd  13096  pcgcd1  13137  pcprmpw2  13142  pcaddlem  13144  fldivp1  13153  4sqlem12  13211  4sqlem14  13213  4sqlem15  13214  4sqlem16  13215  vdwapun  13229  mreexexlem4d  13759  acsfn1  13773  acsfn2  13775  sscpwex  13902  rescabs  13920  catciso  14149  yonedainv  14265  p0le  14359  ple1  14360  subm0  14643  odmodnn0  15065  odeq  15075  dfod2  15087  sylow1lem1  15119  lsmsubg  15175  lsmmod  15194  lsmdisj2  15201  ghmplusg  15348  odadd  15352  gexexlem  15354  lt6abl  15391  cyggex2  15393  ablfacrp  15511  ablfacrp2  15512  ablfac1c  15516  ablfac1eu  15518  lssvancl1  15912  lssvnegcl  15923  lspprvacl  15966  lspsneli  15968  lspsn  15969  lmhmplusg  16011  lmhmima  16014  lmhmpreima  16015  reslmhm  16019  lbsind2  16044  lsmcl  16046  lsmelval2  16048  lsppreli  16053  lspprabs  16058  pj1lmhm  16063  lssvs0or  16073  lspabs3  16084  lspfixed  16091  lspexch  16092  lsmcv  16104  lspsolv  16106  lidlmcl  16179  drngnidl  16191  2idlcpbl  16196  mplbas2  16422  coe1addfv  16552  gzrngunit  16654  zlpirlem3  16660  prmirredlem  16663  znf1o  16722  znunithash  16735  ntrin  17015  topssnei  17078  restbas  17106  restntr  17129  cnntri  17217  fiuncmp  17348  nllyrest  17429  nllyidm  17432  hausllycmp  17437  cldllycmp  17438  hauspwdom  17444  txcld  17515  txcn  17537  txlly  17547  txnlly  17548  txhaus  17558  txlm  17559  txkgen  17563  xkococnlem  17570  cnmpt2res  17588  xkoinjcn  17598  basqtop  17619  qtopeu  17624  qtophmeo  17725  trfbas2  17751  neifil  17788  hausflim  17889  alexsubALTlem2  17955  clssubg  18004  xmetlecl  18124  prdsxmetlem  18145  bldisj  18168  imasf1obl  18247  prdsbl  18250  stdbdmet  18275  stdbdmopn  18277  met2ndci  18281  metcnp  18300  lssnlm  18424  nmotri  18461  nmoid  18464  tgioo  18515  blcvx  18517  xrsmopn  18531  reperflem  18537  reconnlem2  18546  opnreen  18550  metdsge  18567  metdsre  18571  metdscnlem  18573  metnrmlem1a  18576  metnrmlem1  18577  metnrmlem3  18579  cncfmet  18626  cnmpt2pc  18641  icopnfcnv  18655  icopnfhmeo  18656  cnllycmp  18669  evth  18672  lebnumii  18679  nmoleub2lem3  18811  iscfil2  18907  cfil3i  18910  iscfil3  18914  cfilfcls  18915  iscau3  18919  iscmet3lem2  18933  caubl  18948  lmcau  18953  minveclem2  19005  pjthlem1  19016  pjthlem2  19017  ivthicc  19033  ovollecl  19057  ovolunlem1a  19070  ovolunnul  19074  ovoliunlem1  19076  ismbl2  19101  nulmbl2  19109  unmbl  19110  volun  19117  voliunlem2  19123  ioombl1lem2  19131  uniioombllem2a  19152  uniioombllem3  19155  uniioombllem4  19156  dyaddisjlem  19165  dyadmaxlem  19167  opnmbllem  19171  volsup2  19175  volcn  19176  ismbfd  19210  mbfi1fseqlem1  19285  mbfi1fseqlem5  19289  itg2lecl  19308  itg2monolem2  19321  itg2gt0  19330  itgspliticc  19406  ellimc3  19444  limcres  19451  dvfval  19462  dvres3  19478  dvres3a  19479  dvnff  19487  dvnadd  19493  dvn2bss  19494  dvnres  19495  dvcmul  19508  dvcmulf  19509  dvmptres3  19520  dvmptres2  19526  dvmptntr  19535  dvexp3  19540  dvferm1lem  19546  dvlip  19555  dvlipcn  19556  dvlip2  19557  c1liplem1  19558  dvgt0lem1  19564  dvgt0lem2  19565  dvne0  19573  lhop1lem  19575  lhop2  19577  lhop  19578  dvcnvrelem1  19579  dvcnvrelem2  19580  dvcvx  19582  dvfsumle  19583  dvfsumabs  19585  dvfsumlem2  19589  ftc1lem6  19603  ftc1  19604  ftc2ditglem  19607  itgsubstlem  19610  evlslem3  19613  evlslem1  19614  evl1addd  19632  evl1subd  19633  evl1muld  19634  mdegaddle  19675  mdegmullem  19679  ply1rem  19764  fta1glem2  19767  fta1blem  19769  ig1peu  19772  ig1pdvds  19777  dgrmulc  19867  dgrcolem1  19869  plydivlem4  19891  plydiveu  19893  fta1lem  19902  vieta1lem1  19905  vieta1lem2  19906  plyexmo  19908  taylfvallem1  19951  taylfval  19953  tayl0  19956  taylplem1  19957  taylply2  19962  taylply  19963  dvtaylp  19964  dvntaylp  19965  dvntaylp0  19966  taylthlem1  19967  taylthlem2  19968  ulmcaulem  19988  ulmcau  19989  ulmcn  19993  ulmdvlem1  19994  radcnvlem1  20007  radcnvle  20014  psercn  20020  pserdvlem2  20022  pserdv  20023  abelth  20035  cosordlem  20111  tanregt0  20119  dvlog2lem  20221  efopn  20227  logtayllem  20228  logccv  20232  cxplt3  20269  cxpmul2zd  20285  cxpltd  20288  cxpled  20289  cxplt3d  20301  cxple3d  20302  dvsqr  20306  cxpcn3  20310  cxpaddle  20314  cxpeq  20319  angcan  20322  angvald  20324  ang180lem2  20330  ang180lem4  20332  ang180  20334  lawcos  20336  isosctrlem3  20342  dquartlem1  20369  atantayl2  20456  leibpilem1  20458  leibpi  20460  log2tlbnd  20463  birthdaylem3  20470  xrlimcnp  20485  efrlim  20486  o1cxp  20491  jensenlem2  20504  jensen  20505  fsumharmonic  20528  wilthlem1  20529  basellem3  20543  basellem6  20546  basellem8  20548  ppisval  20564  chtwordi  20617  ppiwordi  20623  mumullem2  20641  dvdsmulf1o  20657  fsumvma  20675  fsumvma2  20676  chpchtsum  20681  chpub  20682  logfacubnd  20683  dchrmulcl  20711  dchrinv  20723  dchrptlem1  20726  dchrptlem2  20727  sumdchr2  20732  dchr2sum  20735  bposlem7  20752  lgslem1  20758  lgslem3  20760  lgsdirprm  20791  lgsqrlem2  20804  lgseisenlem1  20811  lgseisenlem2  20812  lgseisenlem4  20814  lgseisen  20815  lgsquadlem1  20816  lgsquad2lem1  20820  lgsquad3  20823  m1lgs  20824  2sqlem7  20832  chebbnd1lem2  20842  chebbnd1lem3  20843  rplogsumlem1  20856  rpvmasumlem  20859  dchrvmasumlem1  20867  dchrvmasum2lem  20868  dchrvmasumlema  20872  dchrisum0flblem2  20881  dchrisum0fno1  20883  dchrisum0re  20885  logdivsum  20905  pntrsumbnd2  20939  pntpbnd1a  20957  pntpbnd1  20958  pntibndlem2  20963  pntlemr  20974  pntlemj  20975  pntlemf  20977  pnt2  20985  padicabv  21002  ostth2lem2  21006  usgraidx2v  21089  nmobndi  21666  ubthlem2  21763  ubthlem3  21764  minvecolem2  21767  shuni  22192  pjhthlem1  22283  chscllem2  22530  pjcompi  22564  mayete3i  22620  mayete3iOLD  22621  unoplin  22813  hmoplin  22835  nmophmi  22924  mdslmd4i  23226  preqsnd  23398  isoun  23492  xrofsup  23526  eliccelico  23541  elicoelioo  23542  difioo  23546  rexdiv  23575  xrge0addgt0  23605  unitdivcld  23654  xrge0mulc1cn  23682  cnextfval  23698  cnextfvval  23701  cnextf  23702  metustto  23796  metustexhalf  23799  cfilucfil  23802  qqhnm  23846  esumcst  23920  esumpcvgval  23933  esumpmono  23934  esumcvg  23941  difelsiga  23981  dya2icoseg  24090  probmeasb  24136  orvcgteel  24173  orvclteel  24178  ballotlemsima  24221  ballotlemfrceq  24234  lgamucov  24270  lgamcvg2  24287  subfacp1lem2a  24314  subfaclim  24322  erdsze2lem2  24338  cvmliftlem2  24420  cvmliftlem10  24428  cvmliftlem13  24430  cvmliftiota  24435  cvmlift2lem9  24445  cvmlift2lem11  24447  cvmlift2lem12  24448  cvmliftphtlem  24451  cvmlift3lem6  24458  cvmlift3lem7  24459  cvmlift3lem9  24461  iseupa  24468  eupap1  24487  eupath2lem3  24490  snmlff  24499  mulge0b  24675  fprodser  24759  fprodshft  24784  fprodrev  24785  rprisefaccl  24812  trpredelss  24976  trpredpo  24979  nodenselem5  25080  nobndlem6  25092  brbtwn2  25275  colinearalglem2  25277  axcgrtr  25285  axcgrid  25286  axsegconlem7  25293  axsegcon  25297  ax5seglem3  25301  ax5seglem6  25304  ax5seg  25308  axpaschlem  25310  axlowdimlem17  25328  axcontlem2  25335  axcontlem4  25337  axcontlem7  25340  axcontlem8  25341  brsegle  25473  bpoly3  25535  itg2addnclem  25675  itg2gt0cn  25678  ftc1cnnclem  25696  ftc1cnnc  25697  areacirclem6  25705  opnregcld  25755  indexdom  25920  sstotbnd2  26004  isbnd3  26014  isbnd3b  26015  cntotbnd  26026  ismtyima  26033  heibor1lem  26039  heiborlem8  26048  rrncmslem  26062  reheibor  26069  lcomfsup  26274  mzpsubst  26332  eldioph2lem1  26345  eldioph2lem2  26346  eldioph2b  26348  diophin  26358  irrapxlem2  26414  irrapxlem4  26416  irrapxlem5  26417  pellexlem1  26420  pellexlem2  26421  pellexlem6  26425  elpell1qr2  26463  pell1qrgaplem  26464  pell1qrgap  26465  pellqrex  26470  pellfundex  26477  pellfund14  26489  rmspecsqrnq  26497  rmxyadd  26512  expmordi  26538  rmxypos  26540  jm2.24  26556  congsub  26563  mzpcong  26565  congrep  26566  acongtr  26571  acongrep  26573  jm2.19lem1  26588  jm2.22  26594  jm2.23  26595  jm2.26lem3  26600  jm2.26  26601  jm2.27a  26604  fnwe2lem2  26654  aomclem6  26662  frlmvscaval  26737  frlmssuvc1  26752  frlmsslsp  26754  frlmup1  26756  frlmup2  26757  enfixsn  26763  lindfind2  26794  lindfrn  26797  f1lindf  26798  islindf4  26814  hbtlem2  26834  hbtlem4  26836  hbtlem5  26838  dgraa0p  26860  rngunsnply  26884  pmtrff1o  26910  pmtrfcnv  26911  pmtrfb  26912  psgnunilem1  26922  mamudi  26967  mamudir  26968  acsfn1p  27013  proot1hash  27025  expgrowth  27058  lkrlsp  29363  lshpkrlem5  29375  ldualssvscl  29419  ldualssvsubcl  29420  llnmlplnN  29799  llncvrlpln  29818  pmapjat1  30113  pclfinN  30160  lautlt  30351  lauteq  30355  lautco  30357  ltrn11  30386  ltrnle  30389  ltrneq2  30408  cdlemednuN  30560  cdleme20k  30579  cdleme20l2  30581  cdleme20l  30582  cdleme20m  30583  cdleme21c  30587  cdleme22e  30604  cdleme22eALTN  30605  cdlemefrs32fva  30660  cdlemg4g  30876  cdlemg18b  30939  cdlemg18c  30940  cdlemj3  31083  dia2dimlem5  31329  dvhopN  31377  cdlemm10N  31379  dihjatcclem4  31682  dochexmidlem2  31722  lclkrlem2o  31782  lcfrlem5  31807  lcfrlem6  31808  lcdlssvscl  31867  mapdpglem6  31939  mapdpglem9  31941  mapdpglem12  31944  mapdpglem14  31946  mapdindp0  31980  hdmaprnlem7N  32119  hdmaprnlem8N  32120  hdmaprnlem3eN  32122  hgmapvvlem3  32189
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 177  df-an 360
  Copyright terms: Public domain W3C validator