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

Theorem syl22anc 1230
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 532 . 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 1227 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  fr2nr  4847  soltmin  5396  f1oprg  5846  fveqf1o  6190  weniso  6235  fr3nr  6600  smogt  7040  smorndom  7041  oacomf1o  7216  difsnen  7601  undom  7607  enfixsn  7628  domss2  7678  ssenen  7693  marypha1lem  7895  fisupcl  7930  ordtypelem3  7948  ordtypelem8  7953  oieu  7967  oismo  7968  wofib  7973  wemaplem2  7975  wemapso  7979  wemapso2OLD  7980  wemapso2lem  7981  unxpwdom2  8017  infdifsn  8076  oemapvali  8106  cantnflem1c  8109  cantnflem1  8111  cantnf  8115  cantnfOLD  8137  cnfcom3  8151  cnfcom3OLD  8159  r1ordg  8199  dif1card  8391  infxpenlem  8394  dfac8clem  8416  infxp  8598  infmap2  8601  cflim2  8646  coftr  8656  fin2i2  8701  enfin2i  8704  fin23lem26  8708  fin23lem27  8711  fin23lem40  8734  isf32lem2  8737  isf32lem3  8738  isf32lem4  8739  isf32lem7  8742  isf32lem9  8744  fin1a2lem13  8795  fin12  8796  alephexp1  8957  gchdomtri  9010  fpwwe2lem12  9022  fpwwe2lem13  9023  gchpwdom  9051  gchhar  9060  adderpqlem  9335  mulerpqlem  9336  addassnq  9339  mulassnq  9340  distrnq  9342  mulidnq  9344  recmulnq  9345  ltexnq  9356  distrlem1pr  9406  distrlem4pr  9407  prlem936  9428  reclem3pr  9430  mulcmpblnr  9451  mulgt0d  9740  mul4d  9795  add4d  9808  add42d  9809  subcan  9879  addsub4d  9983  subadd4d  9984  sub4d  9985  2addsubd  9986  addsubeq4d  9987  muladdd  10020  mulsubd  10021  addgegt0d  10132  addge0d  10134  mulge0d  10135  le2addd  10176  le2subd  10177  ltleaddd  10178  leltaddd  10179  lt2subd  10181  divdivdiv  10251  divcan5  10252  divne0d  10342  recdivd  10343  recdiv2d  10344  divcan6d  10345  ddcand  10346  rec11d  10347  divmuldivd  10367  divmul13d  10368  divmul24d  10369  divadddivd  10370  divsubdivd  10371  divmuleqd  10372  divdivdivd  10373  subrecd  10381  mulge0b  10418  recreclt  10450  divgt0d  10487  mulgt1d  10488  lemulge11d  10489  lemulge12d  10490  ltmul12ad  10493  lemul12ad  10494  lemul12bd  10495  supmul1  10514  nndivtr  10583  qreccl  11211  ledivdivd  11290  lediv12ad  11320  lt2mul2divd  11323  xlt2add  11461  supxrun  11516  supxrre  11528  infmxrre  11536  iccss2  11604  iccssico2  11607  lincmb01cmp  11672  iccf1o  11673  fzrev2i  11753  modaddmodup  12029  modaddmodlo  12030  modsubdir  12034  fzennn  12057  sermono  12118  mulexpz  12185  expaddz  12189  ltexp2a  12196  leexp2a  12200  sqdiv  12212  expmulnbnd  12277  digit1  12279  expsubd  12300  lt2sqd  12323  le2sqd  12324  sq11d  12325  bcm1k  12372  bcp1n  12373  bcp1nk  12374  hashf1lem1  12483  cshw1  12769  2swrd2eqwrdeq  12870  absrele  13120  sqreulem  13171  sqrtmuld  13235  sqrtsq2d  13236  sqrtled  13237  sqrtltd  13238  sqr11d  13239  abs3lemd  13271  rlimuni  13352  climuni  13354  lo1resb  13366  o1resb  13368  2clim  13374  addcn2  13395  mulcn2  13397  o1of2  13414  o1rlimmul  13420  lo1add  13428  lo1mul  13429  isercolllem1  13466  caucvgrlem  13474  iseraltlem2  13484  iseraltlem3  13485  iseralt  13486  mptfzshft  13572  fsumrev  13573  fsum0diag2  13577  binomlem  13620  climcndslem1  13640  climcndslem2  13641  harmonic  13649  mertenslem1  13672  efcllem  13691  moddvds  13870  dvds1  13911  dvdsext  13914  oexpneg  13926  bitsinv1  13969  sadaddlem  13993  sadasslem  13997  sadeq  13999  mulgcd  14061  dvdssqlem  14074  rpmulgcd2  14123  isprm6  14127  isprm5  14130  crt  14185  eulerthlem2  14189  prmdiveq  14193  pythagtriplem11  14226  pythagtriplem13  14228  iserodd  14236  pcgcd1  14277  pcprmpw2  14282  pcaddlem  14284  fldivp1  14293  4sqlem12  14351  4sqlem14  14353  4sqlem15  14354  4sqlem16  14355  vdwapun  14369  mreexexlem4d  14921  acsfn1  14935  acsfn2  14937  sscpwex  15061  rescabs  15079  yonedainv  15424  subm0  15861  pmtrfb  16364  psgnunilem1  16392  odmodnn0  16438  odeq  16448  dfod2  16460  sylow1lem1  16492  lsmsubg  16548  lsmmod  16567  lsmdisj2  16574  ghmplusg  16726  odadd  16730  gexexlem  16732  lt6abl  16771  cyggex2  16773  dprdfinv  16933  dmdprdsplitlem  16958  dpjidcl  16981  ablfacrp  16991  ablfacrp2  16992  ablfac1c  16996  ablfac1eu  16998  lcomfsupOLD  17423  lcomfsupp  17424  lssvancl1  17465  lssvnegcl  17476  lspprvacl  17519  lspsneli  17521  lspsn  17522  lmhmplusg  17564  lmhmima  17567  lmhmpreima  17568  reslmhm  17572  lbsind2  17601  lsmcl  17603  lsmelval2  17605  lsppreli  17610  lspprabs  17615  pj1lmhm  17620  lssvs0or  17630  lspabs3  17641  lspfixed  17648  lspexch  17649  lsmcv  17661  lspsolv  17663  lidlmcl  17739  drngnidl  17751  2idlcpbl  17756  mplbas2  18008  mplbas2OLD  18009  evlslem3  18057  evlslem1  18058  coe1addfv  18180  lply1binom  18222  evl1addd  18251  evl1subd  18252  evl1muld  18253  gzrngunit  18357  zringlpirlem3  18384  zlpirlem3  18389  prmirredlem  18396  prmirredlemOLD  18399  znf1o  18463  znunithash  18476  frlmsubgval  18671  frlmvscaval  18673  frlmphllem  18684  frlmphl  18685  frlmssuvc1  18698  frlmssuvc1OLD  18700  frlmsslsp  18702  frlmsslspOLD  18703  frlmup1  18705  frlmup2  18706  lindfind2  18726  lindfrn  18729  f1lindf  18730  islindf4  18746  mamudi  18778  mamudir  18779  1marepvmarrepid  18950  mdetrlin  18977  smadiadetglem1  19046  smadiadetg  19048  cramerimplem1  19058  mat2pmatscmxcl  19114  m2pmfzgsumcl  19122  pmatcollpw  19155  pmatcollpwfi  19156  pmatcollpw3fi1lem1  19160  cpmidpmatlem2  19245  cpmadugsumlemF  19250  chcoeffeqlem  19259  ntrin  19435  topssnei  19498  restbas  19532  restntr  19556  cnntri  19645  fiuncmp  19777  nllyrest  19860  nllyidm  19863  hausllycmp  19868  cldllycmp  19869  hauspwdom  19875  txcld  19977  txcn  20000  txlly  20010  txnlly  20011  txhaus  20021  txlm  20022  txkgen  20026  xkococnlem  20033  cnmpt2res  20051  xkoinjcn  20061  basqtop  20085  qtopeu  20090  trfbas2  20217  neifil  20254  hausflim  20355  alexsubALTlem2  20421  cnextfval  20435  cnextfvval  20438  cnextf  20439  clssubg  20480  utop2nei  20626  utop3cls  20627  utopreg  20628  psmetlecl  20692  xmetlecl  20722  prdsxmetlem  20744  bldisj  20774  imasf1obl  20864  prdsbl  20867  stdbdmet  20892  stdbdmopn  20894  met2ndci  20898  metcnp  20917  metusttoOLD  20933  metustto  20934  metustexhalfOLD  20939  metustexhalf  20940  cfilucfilOLD  20945  cfilucfil  20946  metucnOLD  20964  metucn  20965  lssnlm  21082  nmotri  21119  nmoid  21122  tgioo  21174  blcvx  21176  xrsmopn  21190  reperflem  21196  reconnlem2  21205  opnreen  21209  metdsge  21226  metdsre  21230  metdscnlem  21232  metnrmlem1a  21235  metnrmlem1  21236  metnrmlem3  21238  cncfmet  21285  cnmpt2pc  21301  icopnfcnv  21315  icopnfhmeo  21316  cnllycmp  21329  evth  21332  lebnumii  21339  nmoleub2lem3  21471  iscfil2  21578  cfil3i  21581  iscfil3  21585  cfilfcls  21586  iscau3  21590  iscmet3lem2  21604  caubl  21619  lmcau  21624  rrxcph  21697  minveclem2  21714  pjthlem1  21725  pjthlem2  21726  ivthicc  21743  ovollecl  21767  ovolunlem1a  21780  ovolunnul  21784  ovoliunlem1  21786  ismbl2  21811  nulmbl2  21820  unmbl  21821  volun  21828  voliunlem2  21834  ioombl1lem2  21842  uniioombllem2a  21864  uniioombllem3  21867  uniioombllem4  21868  dyaddisjlem  21877  dyadmaxlem  21879  opnmbllem  21883  volsup2  21887  volcn  21888  ismbfd  21920  mbfi1fseqlem1  21995  mbfi1fseqlem5  21999  itg2lecl  22018  itg2monolem2  22031  itg2gt0  22040  itgspliticc  22116  ellimc3  22156  limcres  22163  dvfval  22174  dvres3  22190  dvres3a  22191  dvnff  22199  dvnadd  22205  dvn2bss  22206  dvnres  22207  dvcmul  22220  dvcmulf  22221  dvmptres3  22232  dvmptres2  22238  dvmptntr  22247  dvexp3  22252  dvferm1lem  22258  dvlip  22267  dvlipcn  22268  dvlip2  22269  c1liplem1  22270  dvgt0lem1  22276  dvgt0lem2  22277  dvne0  22285  lhop1lem  22287  lhop2  22289  lhop  22290  dvcnvrelem1  22291  dvcnvrelem2  22292  dvcvx  22294  dvfsumle  22295  dvfsumabs  22297  dvfsumlem2  22301  ftc1lem6  22315  ftc1  22316  ftc2ditglem  22319  itgsubstlem  22322  tdeglem4  22331  mdegaddle  22347  mdegmullem  22351  ply1rem  22437  fta1glem2  22440  fta1blem  22442  ig1peu  22445  ig1pdvds  22450  dgrmulc  22540  dgrcolem1  22542  plydivlem4  22564  plydiveu  22566  fta1lem  22575  vieta1lem1  22578  vieta1lem2  22579  plyexmo  22581  taylfvallem1  22624  taylfval  22626  tayl0  22629  taylplem1  22630  taylply2  22635  taylply  22636  dvtaylp  22637  dvntaylp  22638  dvntaylp0  22639  taylthlem1  22640  taylthlem2  22641  ulmcaulem  22661  ulmcau  22662  ulmcn  22666  ulmdvlem1  22667  radcnvlem1  22680  radcnvle  22687  psercn  22693  pserdvlem2  22695  pserdv  22696  abelth  22708  cosordlem  22790  tanregt0  22798  dvlog2lem  22905  efopn  22911  logtayllem  22912  logccv  22916  cxplt3  22953  cxpmul2zd  22969  cxpltd  22972  cxpled  22973  cxplt3d  22985  cxple3d  22986  dvsqrt  22990  cxpcn3  22994  cxpaddle  22998  cxpeq  23003  angcan  23006  angvald  23008  ang180lem2  23014  ang180  23018  isosctrlem3  23026  dquartlem1  23054  atantayl2  23141  leibpilem1  23143  leibpi  23145  log2tlbnd  23148  birthdaylem3  23155  xrlimcnp  23170  efrlim  23171  o1cxp  23176  jensenlem2  23189  jensen  23190  fsumharmonic  23213  wilthlem1  23214  basellem3  23228  basellem6  23231  basellem8  23233  ppisval  23249  chtwordi  23302  ppiwordi  23308  mumullem2  23326  dvdsmulf1o  23342  fsumvma  23360  fsumvma2  23361  chpchtsum  23366  chpub  23367  logfacubnd  23368  dchrmulcl  23396  dchrinv  23408  dchrptlem1  23411  dchrptlem2  23412  sumdchr2  23417  dchr2sum  23420  bposlem7  23437  lgslem1  23443  lgslem3  23445  lgsdirprm  23476  lgsqrlem2  23489  lgseisenlem1  23496  lgseisenlem2  23497  lgseisenlem4  23499  lgseisen  23500  lgsquadlem1  23501  lgsquad2lem1  23505  lgsquad3  23508  m1lgs  23509  2sqlem7  23517  chebbnd1lem2  23527  chebbnd1lem3  23528  rplogsumlem1  23541  rpvmasumlem  23544  dchrvmasumlem1  23552  dchrvmasum2lem  23553  dchrvmasumlema  23557  dchrisum0flblem2  23566  dchrisum0fno1  23568  dchrisum0re  23570  logdivsum  23590  pntrsumbnd2  23624  pntpbnd1a  23642  pntpbnd1  23643  pntibndlem2  23648  pntlemr  23659  pntlemj  23660  pntlemf  23662  pnt2  23670  padicabv  23687  ostth2lem2  23691  f1otrg  24046  brbtwn2  24080  colinearalglem2  24082  axcgrtr  24090  axcgrid  24091  axsegconlem7  24098  axsegcon  24102  ax5seglem3  24106  ax5seglem6  24109  ax5seg  24113  axpaschlem  24115  axlowdimlem17  24133  axcontlem2  24140  axcontlem4  24142  axcontlem7  24145  axcontlem8  24146  ecgrtg  24158  usgraidx2v  24265  iseupa  24837  eupap1  24848  eupath2lem3  24851  numclwwlkovf2ex  24958  nmobndi  25562  ubthlem2  25659  ubthlem3  25660  minvecolem2  25663  shuni  26090  pjhthlem1  26181  chscllem2  26428  pjcompi  26462  mayete3i  26518  mayete3iOLD  26519  unoplin  26711  hmoplin  26733  nmophmi  26822  mdslmd4i  27124  preqsnd  27290  isoun  27392  xrofsup  27454  eliccelico  27460  elicoelioo  27461  difioo  27465  rexdiv  27495  2sqmod  27509  xrge0addgt0  27554  omndadd2d  27571  omndadd2rd  27572  omndmul2  27575  ofldchr  27677  unitdivcld  27756  xrge0mulc1cn  27796  qqhnm  27844  esumcst  27944  esumfsup  27949  esumpmono  27958  esumcvg  27965  difelsiga  28006  1stmbfm  28104  2ndmbfm  28105  dya2icoseg  28121  sibfinima  28154  probmeasb  28242  orvcgteel  28279  orvclteel  28284  ballotlemsima  28327  ballotlemfrceq  28340  sgnmul  28354  ccatmulgnn0dir  28369  ofccat  28370  lgamucov  28453  lgamcvg2  28470  subfacp1lem2a  28497  subfaclim  28505  erdsze2lem2  28521  cvmliftlem2  28604  cvmliftlem10  28612  cvmliftlem13  28614  cvmliftiota  28619  cvmlift2lem9  28629  cvmlift2lem11  28631  cvmlift2lem12  28632  cvmliftphtlem  28635  cvmlift3lem6  28642  cvmlift3lem7  28643  cvmlift3lem9  28645  snmlff  28647  mrsubfval  28741  fprodser  29056  fprodrev  29082  rprisefaccl  29120  trpredelss  29290  trpredpo  29293  wzel  29355  wsuclem  29356  nodenselem5  29420  nobndlem6  29432  brsegle  29733  fin2so  30015  opnmbllem0  30025  mblfinlem3  30028  mblfinlem4  30029  itg2addnclem  30041  itg2addnc  30044  itg2gt0cn  30045  ftc1cnnclem  30063  ftc1cnnc  30064  areacirclem5  30086  opnregcld  30123  indexdom  30200  sstotbnd2  30245  isbnd3  30255  isbnd3b  30256  cntotbnd  30267  ismtyima  30274  heibor1lem  30280  heiborlem8  30289  rrncmslem  30303  reheibor  30310  mzpsubst  30656  eldioph2lem1  30668  eldioph2lem2  30669  eldioph2b  30671  diophin  30681  irrapxlem2  30734  irrapxlem4  30736  irrapxlem5  30737  pellexlem1  30740  pellexlem2  30741  pellexlem6  30745  elpell1qr2  30783  pell1qrgaplem  30784  pell1qrgap  30785  pellqrex  30790  pellfundex  30797  pellfund14  30809  rmspecsqrtnq  30817  rmxyadd  30832  expmordi  30858  rmxypos  30860  jm2.24  30876  congsub  30883  mzpcong  30885  congrep  30886  acongtr  30891  acongrep  30893  jm2.19lem1  30906  jm2.22  30912  jm2.23  30913  jm2.26lem3  30918  jm2.26  30919  jm2.27a  30922  fnwe2lem2  30972  aomclem6  30980  hbtlem2  31048  hbtlem4  31050  hbtlem5  31052  dgraa0p  31074  rngunsnply  31098  acsfn1p  31124  proot1hash  31136  itgpowd  31158  expgrowth  31216  ioondisj2  31461  ioondisj1  31462  elicore  31473  eliocre  31483  ioossioobi  31493  lptioo2  31545  limcresiooub  31556  cncfuni  31596  cncfiooicclem1  31603  dvcnre  31615  dvresntr  31617  dvmptresicc  31620  dvresioo  31622  dvbdfbdioolem1  31629  itgsinexplem1  31642  itgcoscmulx  31658  itgiccshift  31669  itgperiod  31670  stoweidlem11  31682  stoweidlem26  31697  stoweidlem34  31705  stoweidlem36  31707  stoweidlem38  31709  stirlinglem5  31749  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem20  31798  fourierdlem58  31836  fourierdlem72  31850  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem79  31857  fourierdlem80  31858  fourierdlem87  31865  fourierdlem94  31872  fourierdlem103  31881  fourierdlem104  31882  fourierdlem107  31885  fourierdlem113  31891  sqwvfoura  31900  sqwvfourb  31901  fourierswlem  31902  fouriersw  31903  uhgeq12d  32213  usgedgvadf1  32253  usgedgvadf1ALT  32256  lkrlsp  34567  lshpkrlem5  34579  ldualssvscl  34623  ldualssvsubcl  34624  llnmlplnN  35003  llncvrlpln  35022  pmapjat1  35317  pclfinN  35364  lautlt  35555  lauteq  35559  lautco  35561  ltrn11  35590  ltrnle  35593  ltrneq2  35612  cdlemednuN  35765  cdleme20k  35785  cdleme20l2  35787  cdleme20l  35788  cdleme20m  35789  cdleme21c  35793  cdleme22e  35810  cdleme22eALTN  35811  cdlemefrs32fva  35866  cdlemg4g  36082  cdlemg18b  36145  cdlemg18c  36146  cdlemj3  36289  dia2dimlem5  36535  dvhopN  36583  cdlemm10N  36585  dihjatcclem4  36888  dochexmidlem2  36928  lclkrlem2o  36988  lcfrlem5  37013  lcfrlem6  37014  lcdlssvscl  37073  mapdpglem6  37145  mapdpglem9  37147  mapdpglem12  37150  mapdpglem14  37152  mapdindp0  37186  hdmaprnlem7N  37325  hdmaprnlem8N  37326  hdmaprnlem3eN  37328  hgmapvvlem3  37395
  Copyright terms: Public domain W3C validator