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  4370  fr3nr  4570  soltmin  5081  fveqf1o  5768  weniso  5814  smogt  6380  smorndom  6381  oacomf1o  6559  th3qlem1  6760  difsnen  6940  undom  6946  domss2  7016  ssenen  7031  marypha1lem  7182  fisupcl  7214  ordtypelem3  7231  ordtypelem8  7236  oieu  7250  oismo  7251  wofib  7256  wemaplem2  7258  wemapso  7262  wemapso2  7263  unxpwdom2  7298  infdifsn  7353  cantnf  7391  cnfcom3  7403  r1ordg  7446  dif1card  7634  infxpenlem  7637  dfac8clem  7655  infxp  7837  infmap2  7840  cflim2  7885  coftr  7895  fin2i2  7940  enfin2i  7943  fin23lem26  7947  fin23lem27  7950  fin23lem40  7973  isf32lem2  7976  isf32lem3  7977  isf32lem4  7978  isf32lem7  7981  isf32lem9  7983  fin1a2lem13  8034  fin12  8035  alephexp1  8197  gchdomtri  8247  fpwwe2lem12  8259  fpwwe2lem13  8260  gchhar  8289  gchpwdom  8292  adderpqlem  8574  mulerpqlem  8575  addassnq  8578  mulassnq  8579  distrnq  8581  mulidnq  8583  recmulnq  8584  ltexnq  8595  distrlem1pr  8645  distrlem4pr  8646  prlem936  8667  reclem3pr  8669  mulgt0d  8967  mul4d  9020  add4d  9031  add42d  9032  subcan  9098  addsub4d  9200  subadd4d  9201  sub4d  9202  2addsubd  9203  addsubeq4d  9204  muladdd  9233  mulsubd  9234  addgegt0d  9342  addge0d  9344  mulge0d  9345  le2addd  9386  le2subd  9387  ltleaddd  9388  leltaddd  9389  lt2subd  9391  divdivdiv  9457  divcan5  9458  divne0d  9548  recdivd  9549  recdiv2d  9550  divcan6d  9551  ddcand  9552  rec11d  9553  divmuldivd  9573  divmul13d  9574  divmul24d  9575  divadddivd  9576  divsubdivd  9577  divmuleqd  9578  divdivdivd  9579  subrecd  9587  recreclt  9651  divgt0d  9688  mulgt1d  9689  lemulge11d  9690  lemulge12d  9691  ltmul12ad  9694  lemul12ad  9695  lemul12bd  9696  supmul1  9715  nndivtr  9783  qreccl  10332  ledivdivd  10411  lediv12ad  10441  lt2mul2divd  10444  xlt2add  10576  supxrun  10630  supxrre  10642  infmxrre  10650  iccss2  10716  iccssico2  10719  lincmb01cmp  10773  iccf1o  10774  fzrev2i  10844  modsubdir  11004  fzennn  11026  sermono  11074  mulexpz  11138  expaddz  11142  ltexp2a  11149  leexp2a  11153  sqdiv  11165  expmulnbnd  11229  digit1  11231  expsubd  11252  lt2sqd  11275  le2sqd  11276  sq11d  11277  bcm1k  11323  bcp1n  11324  bcp1nk  11325  hashf1lem1  11389  absrele  11789  sqreulem  11839  sqrmuld  11903  sqrsq2d  11904  sqrled  11905  sqrltd  11906  sqr11d  11907  abs3lemd  11939  rlimuni  12020  climuni  12022  lo1resb  12034  o1resb  12036  2clim  12042  addcn2  12063  mulcn2  12065  o1of2  12082  o1rlimmul  12088  lo1add  12096  lo1mul  12097  isercolllem1  12134  caucvgrlem  12141  iseraltlem2  12151  iseraltlem3  12152  iseralt  12153  fsumrev  12237  fsumshft  12238  fsum0diag2  12241  binomlem  12283  climcndslem1  12304  climcndslem2  12305  harmonic  12313  mertenslem1  12336  efcllem  12355  moddvds  12534  dvds1  12573  dvdsext  12575  oexpneg  12586  bitsinv1  12629  sadaddlem  12653  sadasslem  12657  sadeq  12659  mulgcd  12721  dvdssqlem  12734  rpmulgcd2  12780  isprm6  12784  isprm5  12787  crt  12842  eulerthlem2  12846  prmdiveq  12850  pythagtriplem11  12874  pythagtriplem13  12876  iserodd  12884  pcgcd1  12925  pcprmpw2  12930  pcaddlem  12932  fldivp1  12941  4sqlem12  12999  4sqlem14  13001  4sqlem15  13002  4sqlem16  13003  vdwapun  13017  mreexexlem4d  13545  acsfn1  13559  acsfn2  13561  sscpwex  13688  rescabs  13706  catciso  13935  yonedainv  14051  p0le  14145  ple1  14146  subm0  14429  odmodnn0  14851  odeq  14861  dfod2  14873  sylow1lem1  14905  lsmsubg  14961  lsmmod  14980  lsmdisj2  14987  ghmplusg  15134  odadd  15138  gexexlem  15140  lt6abl  15177  cyggex2  15179  ablfacrp  15297  ablfacrp2  15298  ablfac1c  15302  ablfac1eu  15304  lssvancl1  15698  lssvnegcl  15709  lspprvacl  15752  lspsneli  15754  lspsn  15755  lmhmplusg  15797  lmhmima  15800  lmhmpreima  15801  reslmhm  15805  lbsind2  15830  lsmcl  15832  lsmelval2  15834  lsppreli  15839  lspprabs  15844  pj1lmhm  15849  lssvs0or  15859  lspabs3  15870  lspfixed  15877  lspexch  15878  lsmcv  15890  lspsolv  15892  lidlmcl  15965  drngnidl  15977  2idlcpbl  15982  mplbas2  16208  coe1addfv  16338  gzrngunit  16433  zlpirlem3  16439  prmirredlem  16442  znf1o  16501  znunithash  16514  ntrin  16794  topssnei  16857  restbas  16885  restntr  16908  cnntri  16996  fiuncmp  17127  nllyrest  17208  nllyidm  17211  hausllycmp  17216  cldllycmp  17217  hauspwdom  17223  txcld  17294  txcn  17316  txlly  17326  txnlly  17327  txhaus  17337  txlm  17338  txkgen  17342  xkococnlem  17349  cnmpt2res  17367  xkoinjcn  17377  basqtop  17398  qtopeu  17403  qtophmeo  17504  trfbas2  17534  neifil  17571  hausflim  17672  alexsubALTlem2  17738  clssubg  17787  xmetlecl  17907  prdsxmetlem  17928  bldisj  17951  imasf1obl  18030  prdsbl  18033  stdbdmet  18058  stdbdmopn  18060  met2ndci  18064  metcnp  18083  lssnlm  18207  nmotri  18244  nmoid  18247  tgioo  18298  blcvx  18300  xrsmopn  18314  reperflem  18319  reconnlem2  18328  opnreen  18332  metdsge  18349  metdsre  18353  metdscnlem  18355  metnrmlem1a  18358  metnrmlem1  18359  metnrmlem3  18361  cncfmet  18408  cnmpt2pc  18422  icopnfcnv  18436  icopnfhmeo  18437  cnllycmp  18450  evth  18453  lebnumii  18460  nmoleub2lem3  18592  iscfil2  18688  cfil3i  18691  iscfil3  18695  cfilfcls  18696  iscau3  18700  iscmet3lem2  18714  caubl  18729  lmcau  18734  minveclem2  18786  pjthlem1  18797  pjthlem2  18798  ivthicc  18814  ovollecl  18838  ovolunlem1a  18851  ovolunnul  18855  ovoliunlem1  18857  ismbl2  18882  nulmbl2  18890  unmbl  18891  volun  18898  voliunlem2  18904  ioombl1lem2  18912  uniioombllem2a  18933  uniioombllem3  18936  uniioombllem4  18937  dyaddisjlem  18946  dyadmaxlem  18948  opnmbllem  18952  volsup2  18956  volcn  18957  ismbfd  18991  mbfi1fseqlem1  19066  mbfi1fseqlem5  19070  itg2lecl  19089  itg2monolem2  19102  itg2gt0  19111  itgspliticc  19187  ellimc3  19225  limcres  19232  dvfval  19243  dvres3  19259  dvres3a  19260  dvnff  19268  dvnadd  19274  dvn2bss  19275  dvnres  19276  dvcmul  19289  dvcmulf  19290  dvmptres3  19301  dvmptres2  19307  dvmptntr  19316  dvexp3  19321  dvferm1lem  19327  dvlip  19336  dvlipcn  19337  dvlip2  19338  c1liplem1  19339  dvgt0lem1  19345  dvgt0lem2  19346  dvne0  19354  lhop1lem  19356  lhop2  19358  lhop  19359  dvcnvrelem1  19360  dvcnvrelem2  19361  dvcvx  19363  dvfsumle  19364  dvfsumabs  19366  dvfsumlem2  19370  ftc1lem6  19384  ftc1  19385  ftc2ditglem  19388  itgsubstlem  19391  evlslem3  19394  evlslem1  19395  evl1addd  19413  evl1subd  19414  evl1muld  19415  mdegaddle  19456  mdegmullem  19460  ply1rem  19545  fta1glem2  19548  fta1blem  19550  ig1peu  19553  ig1pdvds  19558  dgrmulc  19648  dgrcolem1  19650  plydivlem4  19672  plydiveu  19674  fta1lem  19683  vieta1lem1  19686  vieta1lem2  19687  plyexmo  19689  taylfvallem1  19732  taylfval  19734  tayl0  19737  taylplem1  19738  taylply2  19743  taylply  19744  dvtaylp  19745  dvntaylp  19746  dvntaylp0  19747  taylthlem1  19748  taylthlem2  19749  ulmcaulem  19767  ulmcau  19768  ulmcn  19772  ulmdvlem1  19773  radcnvlem1  19785  radcnvle  19792  psercn  19798  pserdvlem2  19800  pserdv  19801  abelth  19813  cosordlem  19889  tanregt0  19897  dvlog2lem  19995  efopn  20001  logtayllem  20002  logccv  20006  cxplt3  20043  cxpmul2zd  20059  cxpltd  20062  cxpled  20063  cxplt3d  20075  cxple3d  20076  dvsqr  20080  cxpcn3  20084  cxpaddle  20088  cxpeq  20093  angcan  20096  angvald  20098  ang180lem2  20104  ang180lem4  20106  ang180  20108  lawcos  20110  isosctrlem3  20116  dquartlem1  20143  atantayl2  20230  leibpilem1  20232  leibpi  20234  log2tlbnd  20237  birthdaylem3  20244  xrlimcnp  20259  efrlim  20260  o1cxp  20265  jensenlem2  20278  jensen  20279  fsumharmonic  20301  wilthlem1  20302  basellem3  20316  basellem6  20319  basellem8  20321  ppisval  20337  chtwordi  20390  ppiwordi  20396  mumullem2  20414  dvdsmulf1o  20430  fsumvma  20448  fsumvma2  20449  chpchtsum  20454  chpub  20455  logfacubnd  20456  dchrmulcl  20484  dchrinv  20496  dchrptlem1  20499  dchrptlem2  20500  sumdchr2  20505  dchr2sum  20508  bposlem7  20525  lgslem1  20531  lgslem3  20533  lgsdirprm  20564  lgsqrlem2  20577  lgseisenlem1  20584  lgseisenlem2  20585  lgseisenlem4  20587  lgseisen  20588  lgsquadlem1  20589  lgsquad2lem1  20593  lgsquad3  20596  m1lgs  20597  2sqlem7  20605  chebbnd1lem2  20615  chebbnd1lem3  20616  rplogsumlem1  20629  rpvmasumlem  20632  dchrvmasumlem1  20640  dchrvmasum2lem  20641  dchrvmasumlema  20645  dchrisum0flblem2  20654  dchrisum0fno1  20656  dchrisum0re  20658  logdivsum  20678  pntrsumbnd2  20712  pntpbnd1a  20730  pntpbnd1  20731  pntibndlem2  20736  pntlemr  20747  pntlemj  20748  pntlemf  20750  pnt2  20758  padicabv  20775  ostth2lem2  20779  nmobndi  21347  ubthlem2  21444  ubthlem3  21445  minvecolem2  21448  shuni  21875  pjhthlem1  21966  chscllem2  22213  pjcompi  22247  mayete3i  22303  mayete3iOLD  22304  unoplin  22496  hmoplin  22518  nmophmi  22607  mdslmd4i  22909  ballotlemsima  23070  ballotlemfrceq  23083  subfacp1lem2a  23118  subfaclim  23126  erdsze2lem2  23142  cvmliftlem2  23224  cvmliftlem10  23232  cvmliftlem13  23234  cvmliftiota  23239  cvmlift2lem9  23249  cvmlift2lem11  23251  cvmlift2lem12  23252  cvmliftphtlem  23255  cvmlift3lem6  23262  cvmlift3lem7  23263  cvmlift3lem9  23265  iseupa  23288  eupap1  23307  eupath2lem3  23310  snmlff  23319  mulge0b  23492  trpredelss  23639  trpredpo  23642  axdenselem5  23743  axfelem6  23755  axfelem17  23766  brbtwn2  23943  colinearalglem2  23945  axcgrtr  23953  axcgrid  23954  axsegconlem7  23961  axsegcon  23965  ax5seglem3  23969  ax5seglem6  23972  ax5seg  23976  axpaschlem  23978  axlowdimlem17  23996  axcontlem2  24003  axcontlem4  24005  axcontlem7  24008  axcontlem8  24009  brsegle  24141  bpoly3  24203  areacirclem6  24340  infxpg  24505  curgrpact  24783  limptlimpr2lem1  24985  limptlimpr2lem2  24986  cntrset  25013  opnregcld  25659  indexdom  25824  sstotbnd2  25909  isbnd3  25919  isbnd3b  25920  cntotbnd  25931  ismtyima  25938  heibor1lem  25944  heiborlem8  25953  rrncmslem  25967  reheibor  25974  lcomfsup  26179  mzpsubst  26237  eldioph2lem1  26250  eldioph2lem2  26251  eldioph2b  26253  diophin  26263  irrapxlem2  26319  irrapxlem4  26321  irrapxlem5  26322  pellexlem1  26325  pellexlem2  26326  pellexlem6  26330  elpell1qr2  26368  pell1qrgaplem  26369  pell1qrgap  26370  pellqrex  26375  pellfundex  26382  pellfund14  26394  rmspecsqrnq  26402  rmxyadd  26417  expmordi  26443  rmxypos  26445  jm2.24  26461  congsub  26468  mzpcong  26470  congrep  26471  acongtr  26476  acongrep  26478  jm2.19lem1  26493  jm2.22  26499  jm2.23  26500  jm2.26lem3  26505  jm2.26  26506  jm2.27a  26509  fnwe2lem2  26559  aomclem6  26567  frlmvscaval  26642  frlmssuvc1  26657  frlmsslsp  26659  frlmup1  26661  frlmup2  26662  enfixsn  26668  lindfind2  26699  lindfrn  26702  f1lindf  26703  islindf4  26719  hbtlem2  26739  hbtlem4  26741  hbtlem5  26743  dgraa0p  26765  rngunsnply  26789  pmtrff1o  26815  pmtrfcnv  26816  pmtrfb  26817  psgnunilem1  26827  mamudi  26872  mamudir  26873  acsfn1p  26918  proot1hash  26930  expgrowth  26963  lkrlsp  28571  lshpkrlem5  28583  ldualssvscl  28627  ldualssvsubcl  28628  llnmlplnN  29007  llncvrlpln  29026  pmapjat1  29321  pclfinN  29368  lautlt  29559  lauteq  29563  lautco  29565  ltrn11  29594  ltrnle  29597  ltrneq2  29616  cdlemednuN  29768  cdleme20k  29787  cdleme20l2  29789  cdleme20l  29790  cdleme20m  29791  cdleme21c  29795  cdleme22e  29812  cdleme22eALTN  29813  cdlemefrs32fva  29868  cdlemg4g  30084  cdlemg18b  30147  cdlemg18c  30148  cdlemj3  30291  dia2dimlem5  30537  dvhopN  30585  cdlemm10N  30587  dihjatcclem4  30890  dochexmidlem2  30930  lclkrlem2o  30990  lcfrlem5  31015  lcfrlem6  31016  lcdlssvscl  31075  mapdpglem6  31147  mapdpglem9  31149  mapdpglem12  31152  mapdpglem14  31154  mapdindp0  31188  hdmaprnlem7N  31327  hdmaprnlem8N  31328  hdmaprnlem3eN  31330  hgmapvvlem3  31397
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