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

Theorem syl22anc 1265
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 534 . 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 1262 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  fr2nr  4769  soltmin  5193  f1oprg  5810  f1prex  6136  fveqf1o  6154  weniso  6199  fr3nr  6559  smogt  7036  smorndom  7037  oacomf1o  7216  difsnen  7602  undom  7608  enfixsn  7629  domss2  7679  ssenen  7694  marypha1lem  7895  fisupcl  7933  ordtypelem3  7983  ordtypelem8  7988  oieu  8002  oismo  8003  wofib  8008  wemaplem2  8010  wemapso  8014  wemapso2lem  8015  unxpwdom2  8051  infdifsn  8109  oemapvali  8136  cantnflem1c  8139  cantnflem1  8141  cantnf  8145  cnfcom3  8156  r1ordg  8196  dif1card  8388  infxpenlem  8391  dfac8clem  8409  infxp  8591  infmap2  8594  cflim2  8639  coftr  8649  fin2i2  8694  enfin2i  8697  fin23lem26  8701  fin23lem27  8704  fin23lem40  8727  isf32lem2  8730  isf32lem3  8731  isf32lem4  8732  isf32lem7  8735  isf32lem9  8737  fin1a2lem13  8788  fin12  8789  alephexp1  8950  gchdomtri  9000  fpwwe2lem12  9012  fpwwe2lem13  9013  gchpwdom  9041  gchhar  9050  adderpqlem  9325  mulerpqlem  9326  addassnq  9329  mulassnq  9330  distrnq  9332  mulidnq  9334  recmulnq  9335  ltexnq  9346  distrlem1pr  9396  distrlem4pr  9397  prlem936  9418  reclem3pr  9420  mulcmpblnr  9441  mulgt0d  9736  mul4d  9791  add4d  9804  add42d  9805  subcan  9875  addsub4d  9979  subadd4d  9980  sub4d  9981  2addsubd  9982  addsubeq4d  9983  muladdd  10022  mulsubd  10023  addgegt0d  10133  addge0d  10135  mulge0d  10136  le2addd  10178  le2subd  10179  ltleaddd  10180  leltaddd  10181  lt2subd  10183  divdivdiv  10254  divcan5  10255  divne0d  10345  recdivd  10346  recdiv2d  10347  divcan6d  10348  ddcand  10349  rec11d  10350  divmuldivd  10370  divmul13d  10371  divmul24d  10372  divadddivd  10373  divsubdivd  10374  divmuleqd  10375  divdivdivd  10376  subrecd  10384  mulge0b  10421  recreclt  10451  divgt0d  10488  mulgt1d  10489  lemulge11d  10490  lemulge12d  10491  ltmul12ad  10494  lemul12ad  10495  lemul12bd  10496  supmul1  10522  nndivtr  10597  qreccl  11230  ledivdivd  11312  lediv12ad  11343  lt2mul2divd  11351  xlt2add  11492  supxrun  11547  supxrre  11559  infxrre  11568  infmxrreOLD  11572  elicore  11633  iccss2  11651  iccssico2  11654  lincmb01cmp  11721  iccf1o  11722  fzrev2i  11806  modaddmodup  12098  modaddmodlo  12099  modsubdir  12103  fzennn  12126  sermono  12190  mulexpz  12257  expaddz  12261  ltexp2a  12269  leexp2a  12273  sqdiv  12285  expmulnbnd  12349  digit1  12351  expsubd  12372  lt2sqd  12395  le2sqd  12396  sq11d  12397  bcm1k  12445  bcp1n  12446  bcp1nk  12447  hashf1lem1  12561  cshw1  12862  2swrd2eqwrdeq  12967  absrele  13310  sqreulem  13361  sqrtmuld  13425  sqrtsq2d  13426  sqrtled  13427  sqrtltd  13428  sqr11d  13429  abs3lemd  13461  rlimuni  13552  climuni  13554  lo1resb  13566  o1resb  13568  2clim  13574  addcn2  13595  mulcn2  13597  o1of2  13614  o1rlimmul  13620  lo1add  13628  lo1mul  13629  isercolllem1  13666  caucvgrlem  13674  caucvgrlemOLD  13675  iseraltlem2  13687  iseraltlem3  13688  iseralt  13689  mptfzshft  13777  fsumrev  13778  fsum0diag2  13782  binomlem  13825  climcndslem1  13845  climcndslem2  13846  harmonic  13855  mertenslem1  13878  fprodser  13941  fprodrev  13969  rprisefaccl  14014  efcllem  14070  moddvds  14250  dvds1  14291  dvdsext  14294  oexpneg  14306  bitsinv1  14354  sadaddlem  14378  sadasslem  14382  sadeq  14384  mulgcd  14452  dvdssqlem  14465  lcmftp  14547  isprm5  14589  rpmulgcd2  14600  isprm6  14604  coprmproddvdslem  14617  crt  14664  eulerthlem2  14668  prmdiveq  14672  pythagtriplem11  14713  pythagtriplem13  14715  iserodd  14723  pcgcd1  14764  pcprmpw2  14769  pcaddlem  14771  fldivp1  14780  4sqlem12  14838  4sqlem14OLD  14840  4sqlem15OLD  14841  4sqlem16OLD  14842  4sqlem14  14846  4sqlem15  14847  4sqlem16  14848  vdwapun  14862  mreexexlem4d  15491  acsfn1  15505  acsfn2  15507  sscpwex  15658  rescabs  15676  yonedainv  16104  subm0  16541  pmtrfb  17044  psgnunilem1  17072  odmodnn0  17127  odeq  17137  dfod2  17153  sylow1lem1  17188  lsmsubg  17244  lsmmod  17263  lsmdisj2  17270  ghmplusg  17422  odadd  17426  gexexlem  17428  lt6abl  17467  cyggex2  17469  dprdfinv  17590  dmdprdsplitlem  17608  dpjidcl  17629  ablfacrp  17637  ablfacrp2  17638  ablfac1c  17642  ablfac1eu  17644  lcomfsupp  18066  lssvancl1  18106  lssvnegcl  18117  lspprvacl  18160  lspsneli  18162  lspsn  18163  lmhmplusg  18205  lmhmima  18208  lmhmpreima  18209  reslmhm  18213  lbsind2  18242  lsmcl  18244  lsmelval2  18246  lsppreli  18251  lspprabs  18256  pj1lmhm  18261  lssvs0or  18271  lspabs3  18282  lspfixed  18289  lspexch  18290  lsmcv  18302  lspsolv  18304  lidlmcl  18379  drngnidl  18391  2idlcpbl  18396  mplbas2  18632  evlslem3  18675  evlslem1  18676  coe1addfv  18796  lply1binom  18838  evl1addd  18867  evl1subd  18868  evl1muld  18869  gzrngunit  18971  zringlpirlem3OLD  18992  zringlpirlem3  18994  prmirredlem  19001  znf1o  19059  znunithash  19072  frlmsubgval  19264  frlmvscaval  19266  frlmphllem  19275  frlmphl  19276  frlmssuvc1  19289  frlmsslsp  19291  frlmup1  19293  frlmup2  19294  lindfind2  19313  lindfrn  19316  f1lindf  19317  islindf4  19333  mamudi  19365  mamudir  19366  1marepvmarrepid  19537  mdetrlin  19564  smadiadetglem1  19633  smadiadetg  19635  cramerimplem1  19645  mat2pmatscmxcl  19701  m2pmfzgsumcl  19709  pmatcollpw  19742  pmatcollpwfi  19743  pmatcollpw3fi1lem1  19747  cpmidpmatlem2  19832  cpmadugsumlemF  19837  chcoeffeqlem  19846  ntrin  20013  topssnei  20077  restbas  20111  restntr  20135  cnntri  20224  fiuncmp  20356  nllyrest  20438  nllyidm  20441  hausllycmp  20446  cldllycmp  20447  hauspwdom  20453  txcld  20555  txcn  20578  txlly  20588  txnlly  20589  txhaus  20599  txlm  20600  txkgen  20604  xkococnlem  20611  cnmpt2res  20629  xkoinjcn  20639  basqtop  20663  qtopeu  20668  trfbas2  20795  neifil  20832  hausflim  20933  alexsubALTlem2  21000  cnextfval  21014  cnextfvval  21017  cnextf  21018  cnextfres  21021  clssubg  21060  utop2nei  21202  utop3cls  21203  utopreg  21204  psmetlecl  21268  xmetlecl  21298  prdsxmetlem  21320  bldisj  21350  imasf1obl  21440  prdsbl  21443  stdbdmet  21468  stdbdmopn  21470  met2ndci  21474  metcnp  21493  metustto  21505  metustexhalf  21508  cfilucfil  21511  metucn  21523  lssnlm  21640  nmotri  21697  nmoid  21700  tgioo  21751  blcvx  21753  xrsmopn  21767  reperflem  21773  reconnlem2  21782  opnreen  21786  metdsge  21803  metdsre  21807  metdscnlem  21809  metnrmlem1a  21812  metnrmlem1  21813  metnrmlem3  21815  metdsgeOLD  21818  metdsreOLD  21822  metdscnlemOLD  21824  metnrmlem1aOLD  21827  metnrmlem1OLD  21828  metnrmlem3OLD  21830  cncfmet  21877  cnmpt2pc  21893  icopnfcnv  21907  icopnfhmeo  21908  cnllycmp  21921  evth  21924  lebnumii  21934  nmoleub2lem3  22066  iscfil2  22173  cfil3i  22176  iscfil3  22180  cfilfcls  22181  iscau3  22185  iscmet3lem2  22199  caubl  22214  lmcau  22219  rrxcph  22288  minveclem2  22305  minveclem2OLD  22317  pjthlem1  22328  pjthlem2  22329  ivthicc  22346  ovollecl  22373  ovolunlem1a  22386  ovolunnul  22390  ovoliunlem1  22392  ismbl2  22418  nulmbl2  22427  unmbl  22428  volun  22435  voliunlem2  22441  ioombl1lem2  22449  uniioombllem2a  22476  uniioombllem3  22480  uniioombllem4  22481  dyaddisjlem  22490  dyadmaxlem  22492  opnmbllem  22496  volsup2  22500  volcn  22501  ismbfd  22533  mbfi1fseqlem1  22610  mbfi1fseqlem5  22614  itg2lecl  22633  itg2monolem2  22646  itg2gt0  22655  itgspliticc  22731  ellimc3  22771  limcres  22778  dvfval  22789  dvres3  22805  dvres3a  22806  dvnff  22814  dvnadd  22820  dvn2bss  22821  dvnres  22822  dvcmul  22835  dvcmulf  22836  dvmptres3  22847  dvmptres2  22853  dvmptntr  22862  dvexp3  22867  dvferm1lem  22873  dvlip  22882  dvlipcn  22883  dvlip2  22884  c1liplem1  22885  dvgt0lem1  22891  dvgt0lem2  22892  dvne0  22900  lhop1lem  22902  lhop2  22904  lhop  22905  dvcnvrelem1  22906  dvcnvrelem2  22907  dvcvx  22909  dvfsumle  22910  dvfsumabs  22912  dvfsumlem2  22916  ftc1lem6  22930  ftc1  22931  ftc2ditglem  22934  itgsubstlem  22937  tdeglem4  22946  mdegaddle  22960  mdegmullem  22964  ply1rem  23051  fta1glem2  23054  fta1blem  23056  ig1peu  23059  ig1peuOLD  23060  ig1pdvds  23065  ig1pdvdsOLD  23071  dgrmulc  23162  dgrcolem1  23164  plydivlem4  23186  plydiveu  23188  fta1lem  23197  vieta1lem1  23200  vieta1lem2  23201  plyexmo  23203  taylfvallem1  23249  taylfval  23251  tayl0  23254  taylplem1  23255  taylply2  23260  taylply  23261  dvtaylp  23262  dvntaylp  23263  dvntaylp0  23264  taylthlem1  23265  taylthlem2  23266  ulmcaulem  23286  ulmcau  23287  ulmcn  23291  ulmdvlem1  23292  radcnvlem1  23305  radcnvle  23312  psercn  23318  pserdvlem2  23320  pserdv  23321  abelth  23333  cosordlem  23417  tanregt0  23425  dvlog2lem  23534  efopn  23540  logtayllem  23541  logccv  23545  cxplt3  23582  cxpmul2zd  23598  cxpltd  23601  cxpled  23602  cxplt3d  23614  cxple3d  23615  dvsqrt  23619  cxpcn3  23625  cxpaddle  23629  cxpeq  23634  angcan  23668  angvald  23670  ang180lem2  23676  ang180  23680  isosctrlem3  23686  dquartlem1  23714  atantayl2  23801  leibpilem1  23803  leibpi  23805  log2tlbnd  23808  birthdaylem3  23816  xrlimcnp  23831  efrlim  23832  o1cxp  23837  jensenlem2  23850  jensen  23851  fsumharmonic  23874  lgamucov  23900  lgamcvg2  23917  wilthlem1  23930  basellem3  23946  basellem6  23949  basellem8  23951  ppisval  23967  chtwordi  24020  ppiwordi  24026  mumullem2  24044  dvdsmulf1o  24060  fsumvma  24078  fsumvma2  24079  chpchtsum  24084  chpub  24085  logfacubnd  24086  dchrmulcl  24114  dchrinv  24126  dchrptlem1  24129  dchrptlem2  24130  sumdchr2  24135  dchr2sum  24138  bposlem7  24155  lgslem1  24161  lgslem3  24163  lgsdirprm  24194  lgsqrlem2  24207  lgseisenlem1  24214  lgseisenlem2  24215  lgseisenlem4  24217  lgseisen  24218  lgsquadlem1  24219  lgsquad2lem1  24223  lgsquad3  24226  m1lgs  24227  2sqlem7  24235  chebbnd1lem2  24245  chebbnd1lem3  24246  rplogsumlem1  24259  rpvmasumlem  24262  dchrvmasumlem1  24270  dchrvmasum2lem  24271  dchrvmasumlema  24275  dchrisum0flblem2  24284  dchrisum0fno1  24286  dchrisum0re  24288  logdivsum  24308  pntrsumbnd2  24342  pntpbnd1a  24360  pntpbnd1  24361  pntibndlem2  24366  pntlemr  24377  pntlemj  24378  pntlemf  24380  pnt2  24388  padicabv  24405  ostth2lem2  24409  f1otrg  24838  brbtwn2  24872  colinearalglem2  24874  axcgrtr  24882  axcgrid  24883  axsegconlem7  24890  axsegcon  24894  ax5seglem3  24898  ax5seglem6  24901  ax5seg  24905  axpaschlem  24907  axlowdimlem17  24925  axcontlem2  24932  axcontlem4  24934  axcontlem7  24937  axcontlem8  24938  ecgrtg  24950  usgraidx2v  25057  iseupa  25630  eupap1  25641  eupath2lem3  25644  numclwwlkovf2ex  25751  nmobndi  26353  ubthlem2  26450  ubthlem3  26451  minvecolem2  26454  minvecolem2OLD  26464  shuni  26890  pjhthlem1  26981  chscllem2  27228  pjcompi  27262  mayete3i  27318  unoplin  27510  hmoplin  27532  nmophmi  27621  mdslmd4i  27923  preqsnd  28098  isoun  28223  xrge0addcld  28289  xrofsup  28298  eliccelico  28304  elicoelioo  28305  difioo  28309  fz1fzo0m1  28324  rexdiv  28341  2sqmod  28355  xrge0addgt0  28400  omndadd2d  28417  omndadd2rd  28418  omndmul2  28421  ofldchr  28524  mdetpmtr2  28597  mdetpmtr12  28598  madjusmdetlem1  28600  madjusmdetlem4  28603  unitdivcld  28654  xrge0mulc1cn  28694  qqhnm  28741  esumcst  28831  esumfsup  28838  esumpmono  28847  esumcvg  28854  difelsiga  28902  sigapisys  28924  sigapildsys  28931  ldgenpisyslem1  28932  1stmbfm  29029  2ndmbfm  29030  dya2icoseg  29046  sibfinima  29119  probmeasb  29210  orvcgteel  29247  orvclteel  29252  ballotlemsima  29295  ballotlemfrceq  29308  ballotlemsimaOLD  29333  ballotlemfrceqOLD  29346  sgnmul  29360  ccatmulgnn0dir  29375  ofccat  29376  subfacp1lem2a  29850  subfaclim  29858  erdsze2lem2  29874  cvmliftlem2  29956  cvmliftlem10  29964  cvmliftlem13  29966  cvmliftiota  29971  cvmlift2lem9  29981  cvmlift2lem11  29983  cvmlift2lem12  29984  cvmliftphtlem  29987  cvmlift3lem6  29994  cvmlift3lem7  29995  cvmlift3lem9  29997  snmlff  29999  mrsubfval  30093  trpredelss  30419  trpredpo  30422  wzel  30453  wsuclem  30454  nodenselem5  30518  nobndlem6  30530  brsegle  30819  opnregcld  30930  fin2so  31839  poimirlem17  31864  poimirlem23  31870  opnmbllem0  31883  mblfinlem3  31886  mblfinlem4  31887  itg2addnclem  31900  itg2addnc  31903  itg2gt0cn  31904  ftc1cnnclem  31922  ftc1cnnc  31923  areacirclem5  31943  indexdom  31968  sstotbnd2  32013  isbnd3  32023  isbnd3b  32024  cntotbnd  32035  ismtyima  32042  heibor1lem  32048  heiborlem8  32057  rrncmslem  32071  reheibor  32078  lkrlsp  32580  lshpkrlem5  32592  ldualssvscl  32636  ldualssvsubcl  32637  llnmlplnN  33016  llncvrlpln  33035  pmapjat1  33330  pclfinN  33377  lautlt  33568  lauteq  33572  lautco  33574  ltrn11  33603  ltrnle  33606  ltrneq2  33625  cdlemednuN  33778  cdleme20k  33798  cdleme20l2  33800  cdleme20l  33801  cdleme20m  33802  cdleme21c  33806  cdleme22e  33823  cdleme22eALTN  33824  cdlemefrs32fva  33879  cdlemg4g  34095  cdlemg18b  34158  cdlemg18c  34159  cdlemj3  34302  dia2dimlem5  34548  dvhopN  34596  cdlemm10N  34598  dihjatcclem4  34901  dochexmidlem2  34941  lclkrlem2o  35001  lcfrlem5  35026  lcfrlem6  35027  lcdlssvscl  35086  mapdpglem6  35158  mapdpglem9  35160  mapdpglem12  35163  mapdpglem14  35165  mapdindp0  35199  hdmaprnlem7N  35338  hdmaprnlem8N  35339  hdmaprnlem3eN  35341  hgmapvvlem3  35408  mzpsubst  35502  eldioph2lem1  35514  eldioph2lem2  35515  eldioph2b  35517  diophin  35527  irrapxlem2  35580  irrapxlem4  35582  irrapxlem5  35583  pellexlem1  35586  pellexlem2  35587  pellexlem6  35591  elpell1qr2  35631  pell1qrgaplem  35632  pell1qrgap  35633  pellqrex  35639  pellfundex  35647  pellfund14  35659  rmspecsqrtnq  35667  rmxyadd  35682  expmordi  35708  rmxypos  35710  jm2.24  35726  congsub  35733  mzpcong  35735  congrep  35736  acongtr  35741  acongrep  35743  jm2.19lem1  35757  jm2.22  35763  jm2.23  35764  jm2.26lem3  35769  jm2.26  35770  jm2.27a  35773  fnwe2lem2  35822  aomclem6  35830  hbtlem2  35896  hbtlem4  35898  hbtlem5  35900  dgraa0p  35928  rngunsnply  35952  acsfn1p  35978  proot1hash  35990  itgpowd  36012  expgrowth  36597  ioondisj2  37481  ioondisj1  37482  eliocre  37501  ioossioobi  37510  lptioo2  37594  limcresiooub  37606  cncfuni  37647  cncfiooicclem1  37654  cxpcncf2  37661  dvcnre  37669  dvresntr  37671  dvmptresicc  37674  dvresioo  37676  dvbdfbdioolem1  37683  dvnmptdivc  37696  dvnxpaek  37700  itgsinexplem1  37713  itgcoscmulx  37729  itgiccshift  37740  itgperiod  37741  stoweidlem11  37754  stoweidlem26  37769  stoweidlem34  37778  stoweidlem36  37780  stoweidlem38  37782  stirlinglem5  37823  dirkercncflem2  37849  dirkercncflem4  37851  fourierdlem20  37872  fourierdlem58  37911  fourierdlem72  37925  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem79  37932  fourierdlem80  37933  fourierdlem87  37940  fourierdlem94  37947  fourierdlem103  37956  fourierdlem104  37957  fourierdlem107  37960  fourierdlem113  37966  sqwvfoura  37975  sqwvfourb  37976  fourierswlem  37977  fouriersw  37978  etransclem46  38028  etransclem47  38029  sge0ssre  38090  hsphoidmvle2  38254  hsphoidmvle  38255  hoidmv1lelem1  38260  hoidmv1lelem2  38261  hoidmv1lelem3  38262  hoidmvlelem1  38264  iccpartdisj  38564  m1expevenALTV  38590  oexpnegALTV  38619  tgoldbach  38724  usgridx2v  39051  uhgeq12d  39278  usgedgvadf1  39318  usgedgvadf1ALT  39321  nn0eo  39928  fdivpm  39947  refdivpm  39948  elbigolo1  39961  logbpw2m1  39971  fllog2  39972  dignn0flhalflem1  40019  dignn0flhalflem2  40020
  Copyright terms: Public domain W3C validator