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

Theorem syl22anc 1183
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 1180 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  fr2nr  4373  fr3nr  4573  soltmin  5084  fveqf1o  5808  weniso  5854  smogt  6386  smorndom  6387  oacomf1o  6565  th3qlem1  6766  difsnen  6946  undom  6952  domss2  7022  ssenen  7037  marypha1lem  7188  fisupcl  7220  ordtypelem3  7237  ordtypelem8  7242  oieu  7256  oismo  7257  wofib  7262  wemaplem2  7264  wemapso  7268  wemapso2  7269  unxpwdom2  7304  infdifsn  7359  cantnf  7397  cnfcom3  7409  r1ordg  7452  dif1card  7640  infxpenlem  7643  dfac8clem  7661  infxp  7843  infmap2  7846  cflim2  7891  coftr  7901  fin2i2  7946  enfin2i  7949  fin23lem26  7953  fin23lem27  7956  fin23lem40  7979  isf32lem2  7982  isf32lem3  7983  isf32lem4  7984  isf32lem7  7987  isf32lem9  7989  fin1a2lem13  8040  fin12  8041  alephexp1  8203  gchdomtri  8253  fpwwe2lem12  8265  fpwwe2lem13  8266  gchhar  8295  gchpwdom  8298  adderpqlem  8580  mulerpqlem  8581  addassnq  8584  mulassnq  8585  distrnq  8587  mulidnq  8589  recmulnq  8590  ltexnq  8601  distrlem1pr  8651  distrlem4pr  8652  prlem936  8673  reclem3pr  8675  mulgt0d  8973  mul4d  9026  add4d  9037  add42d  9038  subcan  9104  addsub4d  9206  subadd4d  9207  sub4d  9208  2addsubd  9209  addsubeq4d  9210  muladdd  9239  mulsubd  9240  addgegt0d  9348  addge0d  9350  mulge0d  9351  le2addd  9392  le2subd  9393  ltleaddd  9394  leltaddd  9395  lt2subd  9397  divdivdiv  9463  divcan5  9464  divne0d  9554  recdivd  9555  recdiv2d  9556  divcan6d  9557  ddcand  9558  rec11d  9559  divmuldivd  9579  divmul13d  9580  divmul24d  9581  divadddivd  9582  divsubdivd  9583  divmuleqd  9584  divdivdivd  9585  subrecd  9593  recreclt  9657  divgt0d  9694  mulgt1d  9695  lemulge11d  9696  lemulge12d  9697  ltmul12ad  9700  lemul12ad  9701  lemul12bd  9702  supmul1  9721  nndivtr  9789  qreccl  10338  ledivdivd  10417  lediv12ad  10447  lt2mul2divd  10450  xlt2add  10582  supxrun  10636  supxrre  10648  infmxrre  10656  iccss2  10722  iccssico2  10725  lincmb01cmp  10779  iccf1o  10780  fzrev2i  10850  modsubdir  11010  fzennn  11032  sermono  11080  mulexpz  11144  expaddz  11148  ltexp2a  11155  leexp2a  11159  sqdiv  11171  expmulnbnd  11235  digit1  11237  expsubd  11258  lt2sqd  11281  le2sqd  11282  sq11d  11283  bcm1k  11329  bcp1n  11330  bcp1nk  11331  hashf1lem1  11395  absrele  11795  sqreulem  11845  sqrmuld  11909  sqrsq2d  11910  sqrled  11911  sqrltd  11912  sqr11d  11913  abs3lemd  11945  rlimuni  12026  climuni  12028  lo1resb  12040  o1resb  12042  2clim  12048  addcn2  12069  mulcn2  12071  o1of2  12088  o1rlimmul  12094  lo1add  12102  lo1mul  12103  isercolllem1  12140  caucvgrlem  12147  iseraltlem2  12157  iseraltlem3  12158  iseralt  12159  fsumrev  12243  fsumshft  12244  fsum0diag2  12247  binomlem  12289  climcndslem1  12310  climcndslem2  12311  harmonic  12319  mertenslem1  12342  efcllem  12361  moddvds  12540  dvds1  12579  dvdsext  12581  oexpneg  12592  bitsinv1  12635  sadaddlem  12659  sadasslem  12663  sadeq  12665  mulgcd  12727  dvdssqlem  12740  rpmulgcd2  12786  isprm6  12790  isprm5  12793  crt  12848  eulerthlem2  12852  prmdiveq  12856  pythagtriplem11  12880  pythagtriplem13  12882  iserodd  12890  pcgcd1  12931  pcprmpw2  12936  pcaddlem  12938  fldivp1  12947  4sqlem12  13005  4sqlem14  13007  4sqlem15  13008  4sqlem16  13009  vdwapun  13023  mreexexlem4d  13551  acsfn1  13565  acsfn2  13567  sscpwex  13694  rescabs  13712  catciso  13941  yonedainv  14057  p0le  14151  ple1  14152  subm0  14435  odmodnn0  14857  odeq  14867  dfod2  14879  sylow1lem1  14911  lsmsubg  14967  lsmmod  14986  lsmdisj2  14993  ghmplusg  15140  odadd  15144  gexexlem  15146  lt6abl  15183  cyggex2  15185  ablfacrp  15303  ablfacrp2  15304  ablfac1c  15308  ablfac1eu  15310  lssvancl1  15704  lssvnegcl  15715  lspprvacl  15758  lspsneli  15760  lspsn  15761  lmhmplusg  15803  lmhmima  15806  lmhmpreima  15807  reslmhm  15811  lbsind2  15836  lsmcl  15838  lsmelval2  15840  lsppreli  15845  lspprabs  15850  pj1lmhm  15855  lssvs0or  15865  lspabs3  15876  lspfixed  15883  lspexch  15884  lsmcv  15896  lspsolv  15898  lidlmcl  15971  drngnidl  15983  2idlcpbl  15988  mplbas2  16214  coe1addfv  16344  gzrngunit  16439  zlpirlem3  16445  prmirredlem  16448  znf1o  16507  znunithash  16520  ntrin  16800  topssnei  16863  restbas  16891  restntr  16914  cnntri  17002  fiuncmp  17133  nllyrest  17214  nllyidm  17217  hausllycmp  17222  cldllycmp  17223  hauspwdom  17229  txcld  17300  txcn  17322  txlly  17332  txnlly  17333  txhaus  17343  txlm  17344  txkgen  17348  xkococnlem  17355  cnmpt2res  17373  xkoinjcn  17383  basqtop  17404  qtopeu  17409  qtophmeo  17510  trfbas2  17540  neifil  17577  hausflim  17678  alexsubALTlem2  17744  clssubg  17793  xmetlecl  17913  prdsxmetlem  17934  bldisj  17957  imasf1obl  18036  prdsbl  18039  stdbdmet  18064  stdbdmopn  18066  met2ndci  18070  metcnp  18089  lssnlm  18213  nmotri  18250  nmoid  18253  tgioo  18304  blcvx  18306  xrsmopn  18320  reperflem  18325  reconnlem2  18334  opnreen  18338  metdsge  18355  metdsre  18359  metdscnlem  18361  metnrmlem1a  18364  metnrmlem1  18365  metnrmlem3  18367  cncfmet  18414  cnmpt2pc  18428  icopnfcnv  18442  icopnfhmeo  18443  cnllycmp  18456  evth  18459  lebnumii  18466  nmoleub2lem3  18598  iscfil2  18694  cfil3i  18697  iscfil3  18701  cfilfcls  18702  iscau3  18706  iscmet3lem2  18720  caubl  18735  lmcau  18740  minveclem2  18792  pjthlem1  18803  pjthlem2  18804  ivthicc  18820  ovollecl  18844  ovolunlem1a  18857  ovolunnul  18861  ovoliunlem1  18863  ismbl2  18888  nulmbl2  18896  unmbl  18897  volun  18904  voliunlem2  18910  ioombl1lem2  18918  uniioombllem2a  18939  uniioombllem3  18942  uniioombllem4  18943  dyaddisjlem  18952  dyadmaxlem  18954  opnmbllem  18958  volsup2  18962  volcn  18963  ismbfd  18997  mbfi1fseqlem1  19072  mbfi1fseqlem5  19076  itg2lecl  19095  itg2monolem2  19108  itg2gt0  19117  itgspliticc  19193  ellimc3  19231  limcres  19238  dvfval  19249  dvres3  19265  dvres3a  19266  dvnff  19274  dvnadd  19280  dvn2bss  19281  dvnres  19282  dvcmul  19295  dvcmulf  19296  dvmptres3  19307  dvmptres2  19313  dvmptntr  19322  dvexp3  19327  dvferm1lem  19333  dvlip  19342  dvlipcn  19343  dvlip2  19344  c1liplem1  19345  dvgt0lem1  19351  dvgt0lem2  19352  dvne0  19360  lhop1lem  19362  lhop2  19364  lhop  19365  dvcnvrelem1  19366  dvcnvrelem2  19367  dvcvx  19369  dvfsumle  19370  dvfsumabs  19372  dvfsumlem2  19376  ftc1lem6  19390  ftc1  19391  ftc2ditglem  19394  itgsubstlem  19397  evlslem3  19400  evlslem1  19401  evl1addd  19419  evl1subd  19420  evl1muld  19421  mdegaddle  19462  mdegmullem  19466  ply1rem  19551  fta1glem2  19554  fta1blem  19556  ig1peu  19559  ig1pdvds  19564  dgrmulc  19654  dgrcolem1  19656  plydivlem4  19678  plydiveu  19680  fta1lem  19689  vieta1lem1  19692  vieta1lem2  19693  plyexmo  19695  taylfvallem1  19738  taylfval  19740  tayl0  19743  taylplem1  19744  taylply2  19749  taylply  19750  dvtaylp  19751  dvntaylp  19752  dvntaylp0  19753  taylthlem1  19754  taylthlem2  19755  ulmcaulem  19773  ulmcau  19774  ulmcn  19778  ulmdvlem1  19779  radcnvlem1  19791  radcnvle  19798  psercn  19804  pserdvlem2  19806  pserdv  19807  abelth  19819  cosordlem  19895  tanregt0  19903  dvlog2lem  20001  efopn  20007  logtayllem  20008  logccv  20012  cxplt3  20049  cxpmul2zd  20065  cxpltd  20068  cxpled  20069  cxplt3d  20081  cxple3d  20082  dvsqr  20086  cxpcn3  20090  cxpaddle  20094  cxpeq  20099  angcan  20102  angvald  20104  ang180lem2  20110  ang180lem4  20112  ang180  20114  lawcos  20116  isosctrlem3  20122  dquartlem1  20149  atantayl2  20236  leibpilem1  20238  leibpi  20240  log2tlbnd  20243  birthdaylem3  20250  xrlimcnp  20265  efrlim  20266  o1cxp  20271  jensenlem2  20284  jensen  20285  fsumharmonic  20307  wilthlem1  20308  basellem3  20322  basellem6  20325  basellem8  20327  ppisval  20343  chtwordi  20396  ppiwordi  20402  mumullem2  20420  dvdsmulf1o  20436  fsumvma  20454  fsumvma2  20455  chpchtsum  20460  chpub  20461  logfacubnd  20462  dchrmulcl  20490  dchrinv  20502  dchrptlem1  20505  dchrptlem2  20506  sumdchr2  20511  dchr2sum  20514  bposlem7  20531  lgslem1  20537  lgslem3  20539  lgsdirprm  20570  lgsqrlem2  20583  lgseisenlem1  20590  lgseisenlem2  20591  lgseisenlem4  20593  lgseisen  20594  lgsquadlem1  20595  lgsquad2lem1  20599  lgsquad3  20602  m1lgs  20603  2sqlem7  20611  chebbnd1lem2  20621  chebbnd1lem3  20622  rplogsumlem1  20635  rpvmasumlem  20638  dchrvmasumlem1  20646  dchrvmasum2lem  20647  dchrvmasumlema  20651  dchrisum0flblem2  20660  dchrisum0fno1  20662  dchrisum0re  20664  logdivsum  20684  pntrsumbnd2  20718  pntpbnd1a  20736  pntpbnd1  20737  pntibndlem2  20742  pntlemr  20753  pntlemj  20754  pntlemf  20756  pnt2  20764  padicabv  20781  ostth2lem2  20785  nmobndi  21355  ubthlem2  21452  ubthlem3  21453  minvecolem2  21456  shuni  21881  pjhthlem1  21972  chscllem2  22219  pjcompi  22253  mayete3i  22309  mayete3iOLD  22310  unoplin  22502  hmoplin  22524  nmophmi  22613  mdslmd4i  22915  ballotlemsima  23076  ballotlemfrceq  23089  rexdiv  23111  preqsnd  23196  isoun  23244  xrofsup  23257  eliccelico  23272  elicoelioo  23273  difioo  23277  unitdivcld  23287  xrge0mulc1cn  23325  xrge0addgt0  23333  esumcst  23438  esumpcvgval  23448  esumpmono  23449  esumcvg  23456  difelsiga  23496  dya2iocseg  23581  probmeasb  23635  orvcgteel  23670  orvclteel  23675  subfacp1lem2a  23713  subfaclim  23721  erdsze2lem2  23737  cvmliftlem2  23819  cvmliftlem10  23827  cvmliftlem13  23829  cvmliftiota  23834  cvmlift2lem9  23844  cvmlift2lem11  23846  cvmlift2lem12  23847  cvmliftphtlem  23850  cvmlift3lem6  23857  cvmlift3lem7  23858  cvmlift3lem9  23860  iseupa  23883  eupap1  23902  eupath2lem3  23905  snmlff  23914  mulge0b  24088  trpredelss  24237  trpredpo  24240  nodenselem5  24341  nobndlem6  24353  brbtwn2  24535  colinearalglem2  24537  axcgrtr  24545  axcgrid  24546  axsegconlem7  24553  axsegcon  24557  ax5seglem3  24561  ax5seglem6  24564  ax5seg  24568  axpaschlem  24570  axlowdimlem17  24588  axcontlem2  24595  axcontlem4  24597  axcontlem7  24600  axcontlem8  24601  brsegle  24733  bpoly3  24795  itg2addnclem  24933  areacirclem6  24941  infxpg  25106  curgrpact  25383  limptlimpr2lem1  25585  limptlimpr2lem2  25586  cntrset  25613  opnregcld  26259  indexdom  26424  sstotbnd2  26509  isbnd3  26519  isbnd3b  26520  cntotbnd  26531  ismtyima  26538  heibor1lem  26544  heiborlem8  26553  rrncmslem  26567  reheibor  26574  lcomfsup  26779  mzpsubst  26837  eldioph2lem1  26850  eldioph2lem2  26851  eldioph2b  26853  diophin  26863  irrapxlem2  26919  irrapxlem4  26921  irrapxlem5  26922  pellexlem1  26925  pellexlem2  26926  pellexlem6  26930  elpell1qr2  26968  pell1qrgaplem  26969  pell1qrgap  26970  pellqrex  26975  pellfundex  26982  pellfund14  26994  rmspecsqrnq  27002  rmxyadd  27017  expmordi  27043  rmxypos  27045  jm2.24  27061  congsub  27068  mzpcong  27070  congrep  27071  acongtr  27076  acongrep  27078  jm2.19lem1  27093  jm2.22  27099  jm2.23  27100  jm2.26lem3  27105  jm2.26  27106  jm2.27a  27109  fnwe2lem2  27159  aomclem6  27167  frlmvscaval  27242  frlmssuvc1  27257  frlmsslsp  27259  frlmup1  27261  frlmup2  27262  enfixsn  27268  lindfind2  27299  lindfrn  27302  f1lindf  27303  islindf4  27319  hbtlem2  27339  hbtlem4  27341  hbtlem5  27343  dgraa0p  27365  rngunsnply  27389  pmtrff1o  27415  pmtrfcnv  27416  pmtrfb  27417  psgnunilem1  27427  mamudi  27472  mamudir  27473  acsfn1p  27518  proot1hash  27530  expgrowth  27563  f1oprg  28086  lkrlsp  29365  lshpkrlem5  29377  ldualssvscl  29421  ldualssvsubcl  29422  llnmlplnN  29801  llncvrlpln  29820  pmapjat1  30115  pclfinN  30162  lautlt  30353  lauteq  30357  lautco  30359  ltrn11  30388  ltrnle  30391  ltrneq2  30410  cdlemednuN  30562  cdleme20k  30581  cdleme20l2  30583  cdleme20l  30584  cdleme20m  30585  cdleme21c  30589  cdleme22e  30606  cdleme22eALTN  30607  cdlemefrs32fva  30662  cdlemg4g  30878  cdlemg18b  30941  cdlemg18c  30942  cdlemj3  31085  dia2dimlem5  31331  dvhopN  31379  cdlemm10N  31381  dihjatcclem4  31684  dochexmidlem2  31724  lclkrlem2o  31784  lcfrlem5  31809  lcfrlem6  31810  lcdlssvscl  31869  mapdpglem6  31941  mapdpglem9  31943  mapdpglem12  31946  mapdpglem14  31948  mapdindp0  31982  hdmaprnlem7N  32121  hdmaprnlem8N  32122  hdmaprnlem3eN  32124  hgmapvvlem3  32191
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