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  4832  soltmin  5256  f1oprg  5871  f1prex  6197  fveqf1o  6215  weniso  6260  fr3nr  6620  smogt  7094  smorndom  7095  oacomf1o  7274  difsnen  7660  undom  7666  enfixsn  7687  domss2  7737  ssenen  7752  marypha1lem  7953  fisupcl  7991  ordtypelem3  8035  ordtypelem8  8040  oieu  8054  oismo  8055  wofib  8060  wemaplem2  8062  wemapso  8066  wemapso2lem  8067  unxpwdom2  8103  infdifsn  8161  oemapvali  8188  cantnflem1c  8191  cantnflem1  8193  cantnf  8197  cnfcom3  8208  r1ordg  8248  dif1card  8440  infxpenlem  8443  dfac8clem  8461  infxp  8643  infmap2  8646  cflim2  8691  coftr  8701  fin2i2  8746  enfin2i  8749  fin23lem26  8753  fin23lem27  8756  fin23lem40  8779  isf32lem2  8782  isf32lem3  8783  isf32lem4  8784  isf32lem7  8787  isf32lem9  8789  fin1a2lem13  8840  fin12  8841  alephexp1  9002  gchdomtri  9053  fpwwe2lem12  9065  fpwwe2lem13  9066  gchpwdom  9094  gchhar  9103  adderpqlem  9378  mulerpqlem  9379  addassnq  9382  mulassnq  9383  distrnq  9385  mulidnq  9387  recmulnq  9388  ltexnq  9399  distrlem1pr  9449  distrlem4pr  9450  prlem936  9471  reclem3pr  9473  mulcmpblnr  9494  mulgt0d  9789  mul4d  9844  add4d  9857  add42d  9858  subcan  9928  addsub4d  10032  subadd4d  10033  sub4d  10034  2addsubd  10035  addsubeq4d  10036  muladdd  10075  mulsubd  10076  addgegt0d  10186  addge0d  10188  mulge0d  10189  le2addd  10231  le2subd  10232  ltleaddd  10233  leltaddd  10234  lt2subd  10236  divdivdiv  10307  divcan5  10308  divne0d  10398  recdivd  10399  recdiv2d  10400  divcan6d  10401  ddcand  10402  rec11d  10403  divmuldivd  10423  divmul13d  10424  divmul24d  10425  divadddivd  10426  divsubdivd  10427  divmuleqd  10428  divdivdivd  10429  subrecd  10437  mulge0b  10474  recreclt  10505  divgt0d  10542  mulgt1d  10543  lemulge11d  10544  lemulge12d  10545  ltmul12ad  10548  lemul12ad  10549  lemul12bd  10550  supmul1  10576  nndivtr  10651  qreccl  11284  ledivdivd  11366  lediv12ad  11397  lt2mul2divd  11405  xlt2add  11546  supxrun  11601  supxrre  11613  infxrre  11622  infmxrreOLD  11626  elicore  11687  iccss2  11705  iccssico2  11708  lincmb01cmp  11773  iccf1o  11774  fzrev2i  11858  modaddmodup  12150  modaddmodlo  12151  modsubdir  12155  fzennn  12178  sermono  12242  mulexpz  12309  expaddz  12313  ltexp2a  12321  leexp2a  12325  sqdiv  12337  expmulnbnd  12401  digit1  12403  expsubd  12424  lt2sqd  12447  le2sqd  12448  sq11d  12449  bcm1k  12497  bcp1n  12498  bcp1nk  12499  hashf1lem1  12613  cshw1  12906  2swrd2eqwrdeq  13007  absrele  13350  sqreulem  13401  sqrtmuld  13465  sqrtsq2d  13466  sqrtled  13467  sqrtltd  13468  sqr11d  13469  abs3lemd  13501  rlimuni  13592  climuni  13594  lo1resb  13606  o1resb  13608  2clim  13614  addcn2  13635  mulcn2  13637  o1of2  13654  o1rlimmul  13660  lo1add  13668  lo1mul  13669  isercolllem1  13706  caucvgrlem  13714  caucvgrlemOLD  13715  iseraltlem2  13727  iseraltlem3  13728  iseralt  13729  mptfzshft  13817  fsumrev  13818  fsum0diag2  13822  binomlem  13865  climcndslem1  13885  climcndslem2  13886  harmonic  13895  mertenslem1  13918  fprodser  13981  fprodrev  14009  rprisefaccl  14054  efcllem  14110  moddvds  14290  dvds1  14331  dvdsext  14334  oexpneg  14346  bitsinv1  14390  sadaddlem  14414  sadasslem  14418  sadeq  14420  mulgcd  14485  dvdssqlem  14498  lcmftp  14571  isprm5  14613  rpmulgcd2  14624  isprm6  14628  coprmproddvdslem  14641  crt  14686  eulerthlem2  14690  prmdiveq  14694  pythagtriplem11  14729  pythagtriplem13  14731  iserodd  14739  pcgcd1  14780  pcprmpw2  14785  pcaddlem  14787  fldivp1  14796  4sqlem12  14854  4sqlem14OLD  14856  4sqlem15OLD  14857  4sqlem16OLD  14858  4sqlem14  14862  4sqlem15  14863  4sqlem16  14864  vdwapun  14878  mreexexlem4d  15495  acsfn1  15509  acsfn2  15511  sscpwex  15662  rescabs  15680  yonedainv  16108  subm0  16545  pmtrfb  17048  psgnunilem1  17076  odmodnn0  17122  odeq  17132  dfod2  17144  sylow1lem1  17176  lsmsubg  17232  lsmmod  17251  lsmdisj2  17258  ghmplusg  17410  odadd  17414  gexexlem  17416  lt6abl  17455  cyggex2  17457  dprdfinv  17578  dmdprdsplitlem  17596  dpjidcl  17617  ablfacrp  17625  ablfacrp2  17626  ablfac1c  17630  ablfac1eu  17632  lcomfsupp  18054  lssvancl1  18094  lssvnegcl  18105  lspprvacl  18148  lspsneli  18150  lspsn  18151  lmhmplusg  18193  lmhmima  18196  lmhmpreima  18197  reslmhm  18201  lbsind2  18230  lsmcl  18232  lsmelval2  18234  lsppreli  18239  lspprabs  18244  pj1lmhm  18249  lssvs0or  18259  lspabs3  18270  lspfixed  18277  lspexch  18278  lsmcv  18290  lspsolv  18292  lidlmcl  18367  drngnidl  18379  2idlcpbl  18384  mplbas2  18620  evlslem3  18663  evlslem1  18664  coe1addfv  18784  lply1binom  18826  evl1addd  18855  evl1subd  18856  evl1muld  18857  gzrngunit  18959  zringlpirlem3  18980  prmirredlem  18986  znf1o  19044  znunithash  19057  frlmsubgval  19249  frlmvscaval  19251  frlmphllem  19260  frlmphl  19261  frlmssuvc1  19274  frlmsslsp  19276  frlmup1  19278  frlmup2  19279  lindfind2  19298  lindfrn  19301  f1lindf  19302  islindf4  19318  mamudi  19350  mamudir  19351  1marepvmarrepid  19522  mdetrlin  19549  smadiadetglem1  19618  smadiadetg  19620  cramerimplem1  19630  mat2pmatscmxcl  19686  m2pmfzgsumcl  19694  pmatcollpw  19727  pmatcollpwfi  19728  pmatcollpw3fi1lem1  19732  cpmidpmatlem2  19817  cpmadugsumlemF  19822  chcoeffeqlem  19831  ntrin  19998  topssnei  20062  restbas  20096  restntr  20120  cnntri  20209  fiuncmp  20341  nllyrest  20423  nllyidm  20426  hausllycmp  20431  cldllycmp  20432  hauspwdom  20438  txcld  20540  txcn  20563  txlly  20573  txnlly  20574  txhaus  20584  txlm  20585  txkgen  20589  xkococnlem  20596  cnmpt2res  20614  xkoinjcn  20624  basqtop  20648  qtopeu  20653  trfbas2  20780  neifil  20817  hausflim  20918  alexsubALTlem2  20985  cnextfval  20999  cnextfvval  21002  cnextf  21003  cnextfres  21006  clssubg  21045  utop2nei  21187  utop3cls  21188  utopreg  21189  psmetlecl  21253  xmetlecl  21283  prdsxmetlem  21305  bldisj  21335  imasf1obl  21425  prdsbl  21428  stdbdmet  21453  stdbdmopn  21455  met2ndci  21459  metcnp  21478  metustto  21490  metustexhalf  21493  cfilucfil  21496  metucn  21508  lssnlm  21625  nmotri  21662  nmoid  21665  tgioo  21716  blcvx  21718  xrsmopn  21732  reperflem  21738  reconnlem2  21747  opnreen  21751  metdsge  21768  metdsre  21772  metdscnlem  21774  metnrmlem1a  21777  metnrmlem1  21778  metnrmlem3  21780  cncfmet  21827  cnmpt2pc  21843  icopnfcnv  21857  icopnfhmeo  21858  cnllycmp  21871  evth  21874  lebnumii  21881  nmoleub2lem3  22013  iscfil2  22120  cfil3i  22123  iscfil3  22127  cfilfcls  22128  iscau3  22132  iscmet3lem2  22146  caubl  22161  lmcau  22166  rrxcph  22235  minveclem2  22252  pjthlem1  22263  pjthlem2  22264  ivthicc  22281  ovollecl  22305  ovolunlem1a  22318  ovolunnul  22322  ovoliunlem1  22324  ismbl2  22349  nulmbl2  22358  unmbl  22359  volun  22366  voliunlem2  22372  ioombl1lem2  22380  uniioombllem2a  22407  uniioombllem3  22411  uniioombllem4  22412  dyaddisjlem  22421  dyadmaxlem  22423  opnmbllem  22427  volsup2  22431  volcn  22432  ismbfd  22464  mbfi1fseqlem1  22541  mbfi1fseqlem5  22545  itg2lecl  22564  itg2monolem2  22577  itg2gt0  22586  itgspliticc  22662  ellimc3  22702  limcres  22709  dvfval  22720  dvres3  22736  dvres3a  22737  dvnff  22745  dvnadd  22751  dvn2bss  22752  dvnres  22753  dvcmul  22766  dvcmulf  22767  dvmptres3  22778  dvmptres2  22784  dvmptntr  22793  dvexp3  22798  dvferm1lem  22804  dvlip  22813  dvlipcn  22814  dvlip2  22815  c1liplem1  22816  dvgt0lem1  22822  dvgt0lem2  22823  dvne0  22831  lhop1lem  22833  lhop2  22835  lhop  22836  dvcnvrelem1  22837  dvcnvrelem2  22838  dvcvx  22840  dvfsumle  22841  dvfsumabs  22843  dvfsumlem2  22847  ftc1lem6  22861  ftc1  22862  ftc2ditglem  22865  itgsubstlem  22868  tdeglem4  22877  mdegaddle  22891  mdegmullem  22895  ply1rem  22980  fta1glem2  22983  fta1blem  22985  ig1peu  22988  ig1pdvds  22993  dgrmulc  23084  dgrcolem1  23086  plydivlem4  23108  plydiveu  23110  fta1lem  23119  vieta1lem1  23122  vieta1lem2  23123  plyexmo  23125  taylfvallem1  23168  taylfval  23170  tayl0  23173  taylplem1  23174  taylply2  23179  taylply  23180  dvtaylp  23181  dvntaylp  23182  dvntaylp0  23183  taylthlem1  23184  taylthlem2  23185  ulmcaulem  23205  ulmcau  23206  ulmcn  23210  ulmdvlem1  23211  radcnvlem1  23224  radcnvle  23231  psercn  23237  pserdvlem2  23239  pserdv  23240  abelth  23252  cosordlem  23336  tanregt0  23344  dvlog2lem  23453  efopn  23459  logtayllem  23460  logccv  23464  cxplt3  23501  cxpmul2zd  23517  cxpltd  23520  cxpled  23521  cxplt3d  23533  cxple3d  23534  dvsqrt  23538  cxpcn3  23544  cxpaddle  23548  cxpeq  23553  angcan  23587  angvald  23589  ang180lem2  23595  ang180  23599  isosctrlem3  23605  dquartlem1  23633  atantayl2  23720  leibpilem1  23722  leibpi  23724  log2tlbnd  23727  birthdaylem3  23735  xrlimcnp  23750  efrlim  23751  o1cxp  23756  jensenlem2  23769  jensen  23770  fsumharmonic  23793  lgamucov  23819  lgamcvg2  23836  wilthlem1  23849  basellem3  23863  basellem6  23866  basellem8  23868  ppisval  23884  chtwordi  23937  ppiwordi  23943  mumullem2  23961  dvdsmulf1o  23977  fsumvma  23995  fsumvma2  23996  chpchtsum  24001  chpub  24002  logfacubnd  24003  dchrmulcl  24031  dchrinv  24043  dchrptlem1  24046  dchrptlem2  24047  sumdchr2  24052  dchr2sum  24055  bposlem7  24072  lgslem1  24078  lgslem3  24080  lgsdirprm  24111  lgsqrlem2  24124  lgseisenlem1  24131  lgseisenlem2  24132  lgseisenlem4  24134  lgseisen  24135  lgsquadlem1  24136  lgsquad2lem1  24140  lgsquad3  24143  m1lgs  24144  2sqlem7  24152  chebbnd1lem2  24162  chebbnd1lem3  24163  rplogsumlem1  24176  rpvmasumlem  24179  dchrvmasumlem1  24187  dchrvmasum2lem  24188  dchrvmasumlema  24192  dchrisum0flblem2  24201  dchrisum0fno1  24203  dchrisum0re  24205  logdivsum  24225  pntrsumbnd2  24259  pntpbnd1a  24277  pntpbnd1  24278  pntibndlem2  24283  pntlemr  24294  pntlemj  24295  pntlemf  24297  pnt2  24305  padicabv  24322  ostth2lem2  24326  f1otrg  24738  brbtwn2  24772  colinearalglem2  24774  axcgrtr  24782  axcgrid  24783  axsegconlem7  24790  axsegcon  24794  ax5seglem3  24798  ax5seglem6  24801  ax5seg  24805  axpaschlem  24807  axlowdimlem17  24825  axcontlem2  24832  axcontlem4  24834  axcontlem7  24837  axcontlem8  24838  ecgrtg  24850  usgraidx2v  24957  iseupa  25529  eupap1  25540  eupath2lem3  25543  numclwwlkovf2ex  25650  nmobndi  26252  ubthlem2  26349  ubthlem3  26350  minvecolem2  26353  shuni  26779  pjhthlem1  26870  chscllem2  27117  pjcompi  27151  mayete3i  27207  unoplin  27399  hmoplin  27421  nmophmi  27510  mdslmd4i  27812  preqsnd  27987  isoun  28113  xrge0addcld  28174  xrofsup  28180  eliccelico  28186  elicoelioo  28187  difioo  28191  fz1fzo0m1  28206  rexdiv  28224  2sqmod  28238  xrge0addgt0  28283  omndadd2d  28300  omndadd2rd  28301  omndmul2  28304  ofldchr  28407  mdetpmtr2  28480  mdetpmtr12  28481  madjusmdetlem1  28483  madjusmdetlem4  28486  unitdivcld  28537  xrge0mulc1cn  28577  qqhnm  28624  esumcst  28714  esumfsup  28721  esumpmono  28730  esumcvg  28737  difelsiga  28785  sigapisys  28807  sigapildsys  28814  ldgenpisyslem1  28815  1stmbfm  28912  2ndmbfm  28913  dya2icoseg  28929  sibfinima  28991  probmeasb  29080  orvcgteel  29117  orvclteel  29122  ballotlemsima  29165  ballotlemfrceq  29178  sgnmul  29192  ccatmulgnn0dir  29207  ofccat  29208  subfacp1lem2a  29682  subfaclim  29690  erdsze2lem2  29706  cvmliftlem2  29788  cvmliftlem10  29796  cvmliftlem13  29798  cvmliftiota  29803  cvmlift2lem9  29813  cvmlift2lem11  29815  cvmlift2lem12  29816  cvmliftphtlem  29819  cvmlift3lem6  29826  cvmlift3lem7  29827  cvmlift3lem9  29829  snmlff  29831  mrsubfval  29925  trpredelss  30251  trpredpo  30254  wzel  30285  wsuclem  30286  nodenselem5  30350  nobndlem6  30362  brsegle  30651  opnregcld  30762  fin2so  31626  poimirlem17  31651  poimirlem23  31657  opnmbllem0  31670  mblfinlem3  31673  mblfinlem4  31674  itg2addnclem  31687  itg2addnc  31690  itg2gt0cn  31691  ftc1cnnclem  31709  ftc1cnnc  31710  areacirclem5  31730  indexdom  31755  sstotbnd2  31800  isbnd3  31810  isbnd3b  31811  cntotbnd  31822  ismtyima  31829  heibor1lem  31835  heiborlem8  31844  rrncmslem  31858  reheibor  31865  lkrlsp  32367  lshpkrlem5  32379  ldualssvscl  32423  ldualssvsubcl  32424  llnmlplnN  32803  llncvrlpln  32822  pmapjat1  33117  pclfinN  33164  lautlt  33355  lauteq  33359  lautco  33361  ltrn11  33390  ltrnle  33393  ltrneq2  33412  cdlemednuN  33565  cdleme20k  33585  cdleme20l2  33587  cdleme20l  33588  cdleme20m  33589  cdleme21c  33593  cdleme22e  33610  cdleme22eALTN  33611  cdlemefrs32fva  33666  cdlemg4g  33882  cdlemg18b  33945  cdlemg18c  33946  cdlemj3  34089  dia2dimlem5  34335  dvhopN  34383  cdlemm10N  34385  dihjatcclem4  34688  dochexmidlem2  34728  lclkrlem2o  34788  lcfrlem5  34813  lcfrlem6  34814  lcdlssvscl  34873  mapdpglem6  34945  mapdpglem9  34947  mapdpglem12  34950  mapdpglem14  34952  mapdindp0  34986  hdmaprnlem7N  35125  hdmaprnlem8N  35126  hdmaprnlem3eN  35128  hgmapvvlem3  35195  mzpsubst  35289  eldioph2lem1  35301  eldioph2lem2  35302  eldioph2b  35304  diophin  35314  irrapxlem2  35367  irrapxlem4  35369  irrapxlem5  35370  pellexlem1  35373  pellexlem2  35374  pellexlem6  35378  elpell1qr2  35416  pell1qrgaplem  35417  pell1qrgap  35418  pellqrex  35423  pellfundex  35430  pellfund14  35442  rmspecsqrtnq  35450  rmxyadd  35465  expmordi  35491  rmxypos  35493  jm2.24  35509  congsub  35516  mzpcong  35518  congrep  35519  acongtr  35524  acongrep  35526  jm2.19lem1  35540  jm2.22  35546  jm2.23  35547  jm2.26lem3  35552  jm2.26  35553  jm2.27a  35556  fnwe2lem2  35605  aomclem6  35613  hbtlem2  35679  hbtlem4  35681  hbtlem5  35683  dgraa0p  35704  rngunsnply  35728  acsfn1p  35754  proot1hash  35766  itgpowd  35788  expgrowth  36311  ioondisj2  37164  ioondisj1  37165  eliocre  37184  ioossioobi  37193  lptioo2  37273  limcresiooub  37285  cncfuni  37326  cncfiooicclem1  37333  cxpcncf2  37340  dvcnre  37348  dvresntr  37350  dvmptresicc  37353  dvresioo  37355  dvbdfbdioolem1  37362  dvnmptdivc  37372  dvnxpaek  37376  itgsinexplem1  37389  itgcoscmulx  37405  itgiccshift  37416  itgperiod  37417  stoweidlem11  37430  stoweidlem26  37445  stoweidlem34  37454  stoweidlem36  37456  stoweidlem38  37458  stirlinglem5  37499  dirkercncflem2  37525  dirkercncflem4  37527  fourierdlem20  37548  fourierdlem58  37586  fourierdlem72  37600  fourierdlem73  37601  fourierdlem74  37602  fourierdlem75  37603  fourierdlem76  37604  fourierdlem79  37607  fourierdlem80  37608  fourierdlem87  37615  fourierdlem94  37622  fourierdlem103  37631  fourierdlem104  37632  fourierdlem107  37635  fourierdlem113  37641  sqwvfoura  37650  sqwvfourb  37651  fourierswlem  37652  fouriersw  37653  etransclem46  37702  etransclem47  37703  sge0ssre  37763  iccpartdisj  38131  m1expevenALTV  38157  oexpnegALTV  38186  tgoldbach  38291  uhgeq12d  38435  usgedgvadf1  38475  usgedgvadf1ALT  38478  nn0eo  39086  fdivpm  39105  refdivpm  39106  elbigolo1  39119  logbpw2m1  39129  fllog2  39130  dignn0flhalflem1  39177  dignn0flhalflem2  39178
  Copyright terms: Public domain W3C validator