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

Theorem syl22anc 1227
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 530 . 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 1224 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  fr2nr  4771  soltmin  5316  f1oprg  5764  fveqf1o  6106  weniso  6151  fr3nr  6514  smogt  6956  smorndom  6957  oacomf1o  7132  difsnen  7518  undom  7524  enfixsn  7545  domss2  7595  ssenen  7610  marypha1lem  7808  fisupcl  7842  ordtypelem3  7860  ordtypelem8  7865  oieu  7879  oismo  7880  wofib  7885  wemaplem2  7887  wemapso  7891  wemapso2OLD  7892  wemapso2lem  7893  unxpwdom2  7929  infdifsn  7987  oemapvali  8016  cantnflem1c  8019  cantnflem1  8021  cantnf  8025  cantnfOLD  8047  cnfcom3  8061  cnfcom3OLD  8069  r1ordg  8109  dif1card  8301  infxpenlem  8304  dfac8clem  8326  infxp  8508  infmap2  8511  cflim2  8556  coftr  8566  fin2i2  8611  enfin2i  8614  fin23lem26  8618  fin23lem27  8621  fin23lem40  8644  isf32lem2  8647  isf32lem3  8648  isf32lem4  8649  isf32lem7  8652  isf32lem9  8654  fin1a2lem13  8705  fin12  8706  alephexp1  8867  gchdomtri  8918  fpwwe2lem12  8930  fpwwe2lem13  8931  gchpwdom  8959  gchhar  8968  adderpqlem  9243  mulerpqlem  9244  addassnq  9247  mulassnq  9248  distrnq  9250  mulidnq  9252  recmulnq  9253  ltexnq  9264  distrlem1pr  9314  distrlem4pr  9315  prlem936  9336  reclem3pr  9338  mulcmpblnr  9359  mulgt0d  9648  mul4d  9703  add4d  9716  add42d  9717  subcan  9787  addsub4d  9891  subadd4d  9892  sub4d  9893  2addsubd  9894  addsubeq4d  9895  muladdd  9932  mulsubd  9933  addgegt0d  10043  addge0d  10045  mulge0d  10046  le2addd  10087  le2subd  10088  ltleaddd  10089  leltaddd  10090  lt2subd  10092  divdivdiv  10162  divcan5  10163  divne0d  10253  recdivd  10254  recdiv2d  10255  divcan6d  10256  ddcand  10257  rec11d  10258  divmuldivd  10278  divmul13d  10279  divmul24d  10280  divadddivd  10281  divsubdivd  10282  divmuleqd  10283  divdivdivd  10284  subrecd  10292  mulge0b  10329  recreclt  10360  divgt0d  10397  mulgt1d  10398  lemulge11d  10399  lemulge12d  10400  ltmul12ad  10403  lemul12ad  10404  lemul12bd  10405  supmul1  10424  nndivtr  10494  qreccl  11121  ledivdivd  11202  lediv12ad  11232  lt2mul2divd  11235  xlt2add  11373  supxrun  11428  supxrre  11440  infmxrre  11448  iccss2  11516  iccssico2  11519  lincmb01cmp  11584  iccf1o  11585  fzrev2i  11666  modaddmodup  11953  modaddmodlo  11954  modsubdir  11958  fzennn  11981  sermono  12042  mulexpz  12109  expaddz  12113  ltexp2a  12120  leexp2a  12124  sqdiv  12136  expmulnbnd  12200  digit1  12202  expsubd  12223  lt2sqd  12246  le2sqd  12247  sq11d  12248  bcm1k  12295  bcp1n  12296  bcp1nk  12297  hashf1lem1  12408  cshw1  12701  2swrd2eqwrdeq  12802  absrele  13143  sqreulem  13194  sqrtmuld  13258  sqrtsq2d  13259  sqrtled  13260  sqrtltd  13261  sqr11d  13262  abs3lemd  13294  rlimuni  13375  climuni  13377  lo1resb  13389  o1resb  13391  2clim  13397  addcn2  13418  mulcn2  13420  o1of2  13437  o1rlimmul  13443  lo1add  13451  lo1mul  13452  isercolllem1  13489  caucvgrlem  13497  iseraltlem2  13507  iseraltlem3  13508  iseralt  13509  mptfzshft  13595  fsumrev  13596  fsum0diag2  13600  binomlem  13643  climcndslem1  13663  climcndslem2  13664  harmonic  13672  mertenslem1  13695  fprodser  13758  fprodrev  13783  efcllem  13815  moddvds  13995  dvds1  14036  dvdsext  14039  oexpneg  14051  bitsinv1  14094  sadaddlem  14118  sadasslem  14122  sadeq  14124  mulgcd  14186  dvdssqlem  14199  rpmulgcd2  14248  isprm6  14252  isprm5  14255  crt  14310  eulerthlem2  14314  prmdiveq  14318  pythagtriplem11  14351  pythagtriplem13  14353  iserodd  14361  pcgcd1  14402  pcprmpw2  14407  pcaddlem  14409  fldivp1  14418  4sqlem12  14476  4sqlem14  14478  4sqlem15  14479  4sqlem16  14480  vdwapun  14494  mreexexlem4d  15054  acsfn1  15068  acsfn2  15070  sscpwex  15221  rescabs  15239  yonedainv  15667  subm0  16104  pmtrfb  16607  psgnunilem1  16635  odmodnn0  16681  odeq  16691  dfod2  16703  sylow1lem1  16735  lsmsubg  16791  lsmmod  16810  lsmdisj2  16817  ghmplusg  16969  odadd  16973  gexexlem  16975  lt6abl  17014  cyggex2  17016  dprdfinv  17172  dmdprdsplitlem  17197  dpjidcl  17220  ablfacrp  17230  ablfacrp2  17231  ablfac1c  17235  ablfac1eu  17237  lcomfsupOLD  17662  lcomfsupp  17663  lssvancl1  17704  lssvnegcl  17715  lspprvacl  17758  lspsneli  17760  lspsn  17761  lmhmplusg  17803  lmhmima  17806  lmhmpreima  17807  reslmhm  17811  lbsind2  17840  lsmcl  17842  lsmelval2  17844  lsppreli  17849  lspprabs  17854  pj1lmhm  17859  lssvs0or  17869  lspabs3  17880  lspfixed  17887  lspexch  17888  lsmcv  17900  lspsolv  17902  lidlmcl  17978  drngnidl  17990  2idlcpbl  17995  mplbas2  18247  mplbas2OLD  18248  evlslem3  18296  evlslem1  18297  coe1addfv  18419  lply1binom  18461  evl1addd  18490  evl1subd  18491  evl1muld  18492  gzrngunit  18596  zringlpirlem3  18617  prmirredlem  18623  znf1o  18681  znunithash  18694  frlmsubgval  18887  frlmvscaval  18889  frlmphllem  18900  frlmphl  18901  frlmssuvc1  18914  frlmsslsp  18916  frlmup1  18918  frlmup2  18919  lindfind2  18938  lindfrn  18941  f1lindf  18942  islindf4  18958  mamudi  18990  mamudir  18991  1marepvmarrepid  19162  mdetrlin  19189  smadiadetglem1  19258  smadiadetg  19260  cramerimplem1  19270  mat2pmatscmxcl  19326  m2pmfzgsumcl  19334  pmatcollpw  19367  pmatcollpwfi  19368  pmatcollpw3fi1lem1  19372  cpmidpmatlem2  19457  cpmadugsumlemF  19462  chcoeffeqlem  19471  ntrin  19647  topssnei  19711  restbas  19745  restntr  19769  cnntri  19858  fiuncmp  19990  nllyrest  20072  nllyidm  20075  hausllycmp  20080  cldllycmp  20081  hauspwdom  20087  txcld  20189  txcn  20212  txlly  20222  txnlly  20223  txhaus  20233  txlm  20234  txkgen  20238  xkococnlem  20245  cnmpt2res  20263  xkoinjcn  20273  basqtop  20297  qtopeu  20302  trfbas2  20429  neifil  20466  hausflim  20567  alexsubALTlem2  20633  cnextfval  20647  cnextfvval  20650  cnextf  20651  clssubg  20692  utop2nei  20838  utop3cls  20839  utopreg  20840  psmetlecl  20904  xmetlecl  20934  prdsxmetlem  20956  bldisj  20986  imasf1obl  21076  prdsbl  21079  stdbdmet  21104  stdbdmopn  21106  met2ndci  21110  metcnp  21129  metusttoOLD  21145  metustto  21146  metustexhalfOLD  21151  metustexhalf  21152  cfilucfilOLD  21157  cfilucfil  21158  metucnOLD  21176  metucn  21177  lssnlm  21294  nmotri  21331  nmoid  21334  tgioo  21386  blcvx  21388  xrsmopn  21402  reperflem  21408  reconnlem2  21417  opnreen  21421  metdsge  21438  metdsre  21442  metdscnlem  21444  metnrmlem1a  21447  metnrmlem1  21448  metnrmlem3  21450  cncfmet  21497  cnmpt2pc  21513  icopnfcnv  21527  icopnfhmeo  21528  cnllycmp  21541  evth  21544  lebnumii  21551  nmoleub2lem3  21683  iscfil2  21790  cfil3i  21793  iscfil3  21797  cfilfcls  21798  iscau3  21802  iscmet3lem2  21816  caubl  21831  lmcau  21836  rrxcph  21909  minveclem2  21926  pjthlem1  21937  pjthlem2  21938  ivthicc  21955  ovollecl  21979  ovolunlem1a  21992  ovolunnul  21996  ovoliunlem1  21998  ismbl2  22023  nulmbl2  22032  unmbl  22033  volun  22040  voliunlem2  22046  ioombl1lem2  22054  uniioombllem2a  22076  uniioombllem3  22079  uniioombllem4  22080  dyaddisjlem  22089  dyadmaxlem  22091  opnmbllem  22095  volsup2  22099  volcn  22100  ismbfd  22132  mbfi1fseqlem1  22207  mbfi1fseqlem5  22211  itg2lecl  22230  itg2monolem2  22243  itg2gt0  22252  itgspliticc  22328  ellimc3  22368  limcres  22375  dvfval  22386  dvres3  22402  dvres3a  22403  dvnff  22411  dvnadd  22417  dvn2bss  22418  dvnres  22419  dvcmul  22432  dvcmulf  22433  dvmptres3  22444  dvmptres2  22450  dvmptntr  22459  dvexp3  22464  dvferm1lem  22470  dvlip  22479  dvlipcn  22480  dvlip2  22481  c1liplem1  22482  dvgt0lem1  22488  dvgt0lem2  22489  dvne0  22497  lhop1lem  22499  lhop2  22501  lhop  22502  dvcnvrelem1  22503  dvcnvrelem2  22504  dvcvx  22506  dvfsumle  22507  dvfsumabs  22509  dvfsumlem2  22513  ftc1lem6  22527  ftc1  22528  ftc2ditglem  22531  itgsubstlem  22534  tdeglem4  22543  mdegaddle  22559  mdegmullem  22563  ply1rem  22649  fta1glem2  22652  fta1blem  22654  ig1peu  22657  ig1pdvds  22662  dgrmulc  22753  dgrcolem1  22755  plydivlem4  22777  plydiveu  22779  fta1lem  22788  vieta1lem1  22791  vieta1lem2  22792  plyexmo  22794  taylfvallem1  22837  taylfval  22839  tayl0  22842  taylplem1  22843  taylply2  22848  taylply  22849  dvtaylp  22850  dvntaylp  22851  dvntaylp0  22852  taylthlem1  22853  taylthlem2  22854  ulmcaulem  22874  ulmcau  22875  ulmcn  22879  ulmdvlem1  22880  radcnvlem1  22893  radcnvle  22900  psercn  22906  pserdvlem2  22908  pserdv  22909  abelth  22921  cosordlem  23003  tanregt0  23011  dvlog2lem  23120  efopn  23126  logtayllem  23127  logccv  23131  cxplt3  23168  cxpmul2zd  23184  cxpltd  23187  cxpled  23188  cxplt3d  23200  cxple3d  23201  dvsqrt  23205  cxpcn3  23209  cxpaddle  23213  cxpeq  23218  angcan  23252  angvald  23254  ang180lem2  23260  ang180  23264  isosctrlem3  23270  dquartlem1  23298  atantayl2  23385  leibpilem1  23387  leibpi  23389  log2tlbnd  23392  birthdaylem3  23400  xrlimcnp  23415  efrlim  23416  o1cxp  23421  jensenlem2  23434  jensen  23435  fsumharmonic  23458  wilthlem1  23459  basellem3  23473  basellem6  23476  basellem8  23478  ppisval  23494  chtwordi  23547  ppiwordi  23553  mumullem2  23571  dvdsmulf1o  23587  fsumvma  23605  fsumvma2  23606  chpchtsum  23611  chpub  23612  logfacubnd  23613  dchrmulcl  23641  dchrinv  23653  dchrptlem1  23656  dchrptlem2  23657  sumdchr2  23662  dchr2sum  23665  bposlem7  23682  lgslem1  23688  lgslem3  23690  lgsdirprm  23721  lgsqrlem2  23734  lgseisenlem1  23741  lgseisenlem2  23742  lgseisenlem4  23744  lgseisen  23745  lgsquadlem1  23746  lgsquad2lem1  23750  lgsquad3  23753  m1lgs  23754  2sqlem7  23762  chebbnd1lem2  23772  chebbnd1lem3  23773  rplogsumlem1  23786  rpvmasumlem  23789  dchrvmasumlem1  23797  dchrvmasum2lem  23798  dchrvmasumlema  23802  dchrisum0flblem2  23811  dchrisum0fno1  23813  dchrisum0re  23815  logdivsum  23835  pntrsumbnd2  23869  pntpbnd1a  23887  pntpbnd1  23888  pntibndlem2  23893  pntlemr  23904  pntlemj  23905  pntlemf  23907  pnt2  23915  padicabv  23932  ostth2lem2  23936  f1otrg  24295  brbtwn2  24329  colinearalglem2  24331  axcgrtr  24339  axcgrid  24340  axsegconlem7  24347  axsegcon  24351  ax5seglem3  24355  ax5seglem6  24358  ax5seg  24362  axpaschlem  24364  axlowdimlem17  24382  axcontlem2  24389  axcontlem4  24391  axcontlem7  24394  axcontlem8  24395  ecgrtg  24407  usgraidx2v  24514  iseupa  25086  eupap1  25097  eupath2lem3  25100  numclwwlkovf2ex  25207  nmobndi  25807  ubthlem2  25904  ubthlem3  25905  minvecolem2  25908  shuni  26335  pjhthlem1  26426  chscllem2  26673  pjcompi  26707  mayete3i  26763  unoplin  26955  hmoplin  26977  nmophmi  27066  mdslmd4i  27368  preqsnd  27543  isoun  27667  xrge0addcld  27732  xrofsup  27735  eliccelico  27741  elicoelioo  27742  difioo  27746  rexdiv  27775  2sqmod  27789  xrge0addgt0  27834  omndadd2d  27851  omndadd2rd  27852  omndmul2  27855  ofldchr  27958  unitdivcld  28037  xrge0mulc1cn  28077  qqhnm  28124  esumcst  28211  esumfsup  28218  esumpmono  28227  esumcvg  28234  difelsiga  28282  sigapisys  28303  sigapildsys  28307  1stmbfm  28387  2ndmbfm  28388  dya2icoseg  28404  sibfinima  28464  probmeasb  28552  orvcgteel  28589  orvclteel  28594  ballotlemsima  28637  ballotlemfrceq  28650  sgnmul  28664  ccatmulgnn0dir  28679  ofccat  28680  lgamucov  28769  lgamcvg2  28786  subfacp1lem2a  28813  subfaclim  28821  erdsze2lem2  28837  cvmliftlem2  28920  cvmliftlem10  28928  cvmliftlem13  28930  cvmliftiota  28935  cvmlift2lem9  28945  cvmlift2lem11  28947  cvmlift2lem12  28948  cvmliftphtlem  28951  cvmlift3lem6  28958  cvmlift3lem7  28959  cvmlift3lem9  28961  snmlff  28963  mrsubfval  29057  rprisefaccl  29311  trpredelss  29480  trpredpo  29483  wzel  29545  wsuclem  29546  nodenselem5  29610  nobndlem6  29622  brsegle  29911  fin2so  30205  opnmbllem0  30215  mblfinlem3  30218  mblfinlem4  30219  itg2addnclem  30232  itg2addnc  30235  itg2gt0cn  30236  ftc1cnnclem  30254  ftc1cnnc  30255  areacirclem5  30277  opnregcld  30314  indexdom  30391  sstotbnd2  30436  isbnd3  30446  isbnd3b  30447  cntotbnd  30458  ismtyima  30465  heibor1lem  30471  heiborlem8  30480  rrncmslem  30494  reheibor  30501  mzpsubst  30846  eldioph2lem1  30858  eldioph2lem2  30859  eldioph2b  30861  diophin  30871  irrapxlem2  30924  irrapxlem4  30926  irrapxlem5  30927  pellexlem1  30930  pellexlem2  30931  pellexlem6  30935  elpell1qr2  30973  pell1qrgaplem  30974  pell1qrgap  30975  pellqrex  30980  pellfundex  30987  pellfund14  30999  rmspecsqrtnq  31007  rmxyadd  31022  expmordi  31048  rmxypos  31050  jm2.24  31066  congsub  31073  mzpcong  31075  congrep  31076  acongtr  31081  acongrep  31083  jm2.19lem1  31097  jm2.22  31103  jm2.23  31104  jm2.26lem3  31109  jm2.26  31110  jm2.27a  31113  fnwe2lem2  31163  aomclem6  31171  hbtlem2  31241  hbtlem4  31243  hbtlem5  31245  dgraa0p  31266  rngunsnply  31290  acsfn1p  31316  proot1hash  31328  itgpowd  31350  expgrowth  31408  ioondisj2  31691  ioondisj1  31692  elicore  31703  eliocre  31713  ioossioobi  31723  lptioo2  31803  limcresiooub  31814  cncfuni  31855  cncfiooicclem1  31862  cxpcncf2  31869  dvcnre  31877  dvresntr  31879  dvmptresicc  31882  dvresioo  31884  dvbdfbdioolem1  31891  dvnmptdivc  31901  dvnxpaek  31905  itgsinexplem1  31918  itgcoscmulx  31934  itgiccshift  31945  itgperiod  31946  stoweidlem11  31959  stoweidlem26  31974  stoweidlem34  31982  stoweidlem36  31984  stoweidlem38  31986  stirlinglem5  32026  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem20  32075  fourierdlem58  32113  fourierdlem72  32127  fourierdlem73  32128  fourierdlem74  32129  fourierdlem75  32130  fourierdlem76  32131  fourierdlem79  32134  fourierdlem80  32135  fourierdlem87  32142  fourierdlem94  32149  fourierdlem103  32158  fourierdlem104  32159  fourierdlem107  32162  fourierdlem113  32168  sqwvfoura  32177  sqwvfourb  32178  fourierswlem  32179  fouriersw  32180  etransclem46  32229  etransclem47  32230  m1expevenALTV  32490  oexpnegALTV  32519  uhgeq12d  32693  usgedgvadf1  32733  usgedgvadf1ALT  32736  nn0eo  33345  fdivpm  33364  refdivpm  33365  elbigolo1  33378  logbpw2m1  33388  fllog2  33389  dignn0flhalflem1  33436  dignn0flhalflem2  33437  lkrlsp  35240  lshpkrlem5  35252  ldualssvscl  35296  ldualssvsubcl  35297  llnmlplnN  35676  llncvrlpln  35695  pmapjat1  35990  pclfinN  36037  lautlt  36228  lauteq  36232  lautco  36234  ltrn11  36263  ltrnle  36266  ltrneq2  36285  cdlemednuN  36438  cdleme20k  36458  cdleme20l2  36460  cdleme20l  36461  cdleme20m  36462  cdleme21c  36466  cdleme22e  36483  cdleme22eALTN  36484  cdlemefrs32fva  36539  cdlemg4g  36755  cdlemg18b  36818  cdlemg18c  36819  cdlemj3  36962  dia2dimlem5  37208  dvhopN  37256  cdlemm10N  37258  dihjatcclem4  37561  dochexmidlem2  37601  lclkrlem2o  37661  lcfrlem5  37686  lcfrlem6  37687  lcdlssvscl  37746  mapdpglem6  37818  mapdpglem9  37820  mapdpglem12  37823  mapdpglem14  37825  mapdindp0  37859  hdmaprnlem7N  37998  hdmaprnlem8N  37999  hdmaprnlem3eN  38001  hgmapvvlem3  38068
  Copyright terms: Public domain W3C validator