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

Theorem syl22anc 1186
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 520 . 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 1183 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  fr2nr  4562  fr3nr  4762  soltmin  5275  f1oprg  5720  fveqf1o  6031  weniso  6077  smogt  6631  smorndom  6632  oacomf1o  6810  th3qlem1  7012  difsnen  7192  undom  7198  domss2  7268  ssenen  7283  marypha1lem  7440  fisupcl  7474  ordtypelem3  7491  ordtypelem8  7496  oieu  7510  oismo  7511  wofib  7516  wemaplem2  7518  wemapso  7522  wemapso2  7523  unxpwdom2  7558  infdifsn  7613  cantnf  7651  cnfcom3  7663  r1ordg  7706  dif1card  7894  infxpenlem  7897  dfac8clem  7915  infxp  8097  infmap2  8100  cflim2  8145  coftr  8155  fin2i2  8200  enfin2i  8203  fin23lem26  8207  fin23lem27  8210  fin23lem40  8233  isf32lem2  8236  isf32lem3  8237  isf32lem4  8238  isf32lem7  8241  isf32lem9  8243  fin1a2lem13  8294  fin12  8295  alephexp1  8456  gchdomtri  8506  fpwwe2lem12  8518  fpwwe2lem13  8519  gchhar  8548  gchpwdom  8551  adderpqlem  8833  mulerpqlem  8834  addassnq  8837  mulassnq  8838  distrnq  8840  mulidnq  8842  recmulnq  8843  ltexnq  8854  distrlem1pr  8904  distrlem4pr  8905  prlem936  8926  reclem3pr  8928  mulgt0d  9227  mul4d  9280  add4d  9291  add42d  9292  subcan  9358  addsub4d  9460  subadd4d  9461  sub4d  9462  2addsubd  9463  addsubeq4d  9464  muladdd  9493  mulsubd  9494  addgegt0d  9602  addge0d  9604  mulge0d  9605  le2addd  9646  le2subd  9647  ltleaddd  9648  leltaddd  9649  lt2subd  9651  divdivdiv  9717  divcan5  9718  divne0d  9808  recdivd  9809  recdiv2d  9810  divcan6d  9811  ddcand  9812  rec11d  9813  divmuldivd  9833  divmul13d  9834  divmul24d  9835  divadddivd  9836  divsubdivd  9837  divmuleqd  9838  divdivdivd  9839  subrecd  9847  recreclt  9911  divgt0d  9948  mulgt1d  9949  lemulge11d  9950  lemulge12d  9951  ltmul12ad  9954  lemul12ad  9955  lemul12bd  9956  supmul1  9975  nndivtr  10043  qreccl  10596  ledivdivd  10675  lediv12ad  10705  lt2mul2divd  10708  xlt2add  10841  supxrun  10896  supxrre  10908  infmxrre  10916  iccss2  10983  iccssico2  10986  lincmb01cmp  11040  iccf1o  11041  fzrev2i  11112  modsubdir  11287  fzennn  11309  sermono  11357  mulexpz  11422  expaddz  11426  ltexp2a  11433  leexp2a  11437  sqdiv  11449  expmulnbnd  11513  digit1  11515  expsubd  11536  lt2sqd  11559  le2sqd  11560  sq11d  11561  bcm1k  11608  bcp1n  11609  bcp1nk  11610  hashf1lem1  11706  absrele  12115  sqreulem  12165  sqrmuld  12229  sqrsq2d  12230  sqrled  12231  sqrltd  12232  sqr11d  12233  abs3lemd  12265  rlimuni  12346  climuni  12348  lo1resb  12360  o1resb  12362  2clim  12368  addcn2  12389  mulcn2  12391  o1of2  12408  o1rlimmul  12414  lo1add  12422  lo1mul  12423  isercolllem1  12460  caucvgrlem  12468  iseraltlem2  12478  iseraltlem3  12479  iseralt  12480  fsumrev  12564  fsumshft  12565  fsum0diag2  12568  binomlem  12610  climcndslem1  12631  climcndslem2  12632  harmonic  12640  mertenslem1  12663  efcllem  12682  moddvds  12861  dvds1  12900  dvdsext  12902  oexpneg  12913  bitsinv1  12956  sadaddlem  12980  sadasslem  12984  sadeq  12986  mulgcd  13048  dvdssqlem  13061  rpmulgcd2  13107  isprm6  13111  isprm5  13114  crt  13169  eulerthlem2  13173  prmdiveq  13177  pythagtriplem11  13201  pythagtriplem13  13203  iserodd  13211  pcgcd1  13252  pcprmpw2  13257  pcaddlem  13259  fldivp1  13268  4sqlem12  13326  4sqlem14  13328  4sqlem15  13329  4sqlem16  13330  vdwapun  13344  mreexexlem4d  13874  acsfn1  13888  acsfn2  13890  sscpwex  14017  rescabs  14035  catciso  14264  yonedainv  14380  p0le  14474  ple1  14475  subm0  14758  odmodnn0  15180  odeq  15190  dfod2  15202  sylow1lem1  15234  lsmsubg  15290  lsmmod  15309  lsmdisj2  15316  ghmplusg  15463  odadd  15467  gexexlem  15469  lt6abl  15506  cyggex2  15508  ablfacrp  15626  ablfacrp2  15627  ablfac1c  15631  ablfac1eu  15633  lssvancl1  16023  lssvnegcl  16034  lspprvacl  16077  lspsneli  16079  lspsn  16080  lmhmplusg  16122  lmhmima  16125  lmhmpreima  16126  reslmhm  16130  lbsind2  16155  lsmcl  16157  lsmelval2  16159  lsppreli  16164  lspprabs  16169  pj1lmhm  16174  lssvs0or  16184  lspabs3  16195  lspfixed  16202  lspexch  16203  lsmcv  16215  lspsolv  16217  lidlmcl  16290  drngnidl  16302  2idlcpbl  16307  mplbas2  16533  coe1addfv  16660  gzrngunit  16766  zlpirlem3  16772  prmirredlem  16775  znf1o  16834  znunithash  16847  ntrin  17127  topssnei  17190  restbas  17224  restntr  17248  cnntri  17337  fiuncmp  17469  nllyrest  17551  nllyidm  17554  hausllycmp  17559  cldllycmp  17560  hauspwdom  17566  txcld  17637  txcn  17660  txlly  17670  txnlly  17671  txhaus  17681  txlm  17682  txkgen  17686  xkococnlem  17693  cnmpt2res  17711  xkoinjcn  17721  basqtop  17745  qtopeu  17750  qtophmeo  17851  trfbas2  17877  neifil  17914  hausflim  18015  alexsubALTlem2  18081  cnextfval  18095  cnextfvval  18098  cnextf  18099  clssubg  18140  utop2nei  18282  utop3cls  18283  utopreg  18284  psmetlecl  18348  xmetlecl  18378  prdsxmetlem  18400  bldisj  18430  imasf1obl  18520  prdsbl  18523  stdbdmet  18548  stdbdmopn  18550  met2ndci  18554  metcnp  18573  metusttoOLD  18589  metustto  18590  metustexhalfOLD  18595  metustexhalf  18596  cfilucfilOLD  18601  cfilucfil  18602  metucnOLD  18620  metucn  18621  lssnlm  18738  nmotri  18775  nmoid  18778  tgioo  18829  blcvx  18831  xrsmopn  18845  reperflem  18851  reconnlem2  18860  opnreen  18864  metdsge  18881  metdsre  18885  metdscnlem  18887  metnrmlem1a  18890  metnrmlem1  18891  metnrmlem3  18893  cncfmet  18940  cnmpt2pc  18955  icopnfcnv  18969  icopnfhmeo  18970  cnllycmp  18983  evth  18986  lebnumii  18993  nmoleub2lem3  19125  iscfil2  19221  cfil3i  19224  iscfil3  19228  cfilfcls  19229  iscau3  19233  iscmet3lem2  19247  caubl  19262  lmcau  19267  minveclem2  19329  pjthlem1  19340  pjthlem2  19341  ivthicc  19357  ovollecl  19381  ovolunlem1a  19394  ovolunnul  19398  ovoliunlem1  19400  ismbl2  19425  nulmbl2  19433  unmbl  19434  volun  19441  voliunlem2  19447  ioombl1lem2  19455  uniioombllem2a  19476  uniioombllem3  19479  uniioombllem4  19480  dyaddisjlem  19489  dyadmaxlem  19491  opnmbllem  19495  volsup2  19499  volcn  19500  ismbfd  19534  mbfi1fseqlem1  19609  mbfi1fseqlem5  19613  itg2lecl  19632  itg2monolem2  19645  itg2gt0  19654  itgspliticc  19730  ellimc3  19768  limcres  19775  dvfval  19786  dvres3  19802  dvres3a  19803  dvnff  19811  dvnadd  19817  dvn2bss  19818  dvnres  19819  dvcmul  19832  dvcmulf  19833  dvmptres3  19844  dvmptres2  19850  dvmptntr  19859  dvexp3  19864  dvferm1lem  19870  dvlip  19879  dvlipcn  19880  dvlip2  19881  c1liplem1  19882  dvgt0lem1  19888  dvgt0lem2  19889  dvne0  19897  lhop1lem  19899  lhop2  19901  lhop  19902  dvcnvrelem1  19903  dvcnvrelem2  19904  dvcvx  19906  dvfsumle  19907  dvfsumabs  19909  dvfsumlem2  19913  ftc1lem6  19927  ftc1  19928  ftc2ditglem  19931  itgsubstlem  19934  evlslem3  19937  evlslem1  19938  evl1addd  19956  evl1subd  19957  evl1muld  19958  mdegaddle  19999  mdegmullem  20003  ply1rem  20088  fta1glem2  20091  fta1blem  20093  ig1peu  20096  ig1pdvds  20101  dgrmulc  20191  dgrcolem1  20193  plydivlem4  20215  plydiveu  20217  fta1lem  20226  vieta1lem1  20229  vieta1lem2  20230  plyexmo  20232  taylfvallem1  20275  taylfval  20277  tayl0  20280  taylplem1  20281  taylply2  20286  taylply  20287  dvtaylp  20288  dvntaylp  20289  dvntaylp0  20290  taylthlem1  20291  taylthlem2  20292  ulmcaulem  20312  ulmcau  20313  ulmcn  20317  ulmdvlem1  20318  radcnvlem1  20331  radcnvle  20338  psercn  20344  pserdvlem2  20346  pserdv  20347  abelth  20359  cosordlem  20435  tanregt0  20443  dvlog2lem  20545  efopn  20551  logtayllem  20552  logccv  20556  cxplt3  20593  cxpmul2zd  20609  cxpltd  20612  cxpled  20613  cxplt3d  20625  cxple3d  20626  dvsqr  20630  cxpcn3  20634  cxpaddle  20638  cxpeq  20643  angcan  20646  angvald  20648  ang180lem2  20654  ang180  20658  isosctrlem3  20666  dquartlem1  20693  atantayl2  20780  leibpilem1  20782  leibpi  20784  log2tlbnd  20787  birthdaylem3  20794  xrlimcnp  20809  efrlim  20810  o1cxp  20815  jensenlem2  20828  jensen  20829  fsumharmonic  20852  wilthlem1  20853  basellem3  20867  basellem6  20870  basellem8  20872  ppisval  20888  chtwordi  20941  ppiwordi  20947  mumullem2  20965  dvdsmulf1o  20981  fsumvma  20999  fsumvma2  21000  chpchtsum  21005  chpub  21006  logfacubnd  21007  dchrmulcl  21035  dchrinv  21047  dchrptlem1  21050  dchrptlem2  21051  sumdchr2  21056  dchr2sum  21059  bposlem7  21076  lgslem1  21082  lgslem3  21084  lgsdirprm  21115  lgsqrlem2  21128  lgseisenlem1  21135  lgseisenlem2  21136  lgseisenlem4  21138  lgseisen  21139  lgsquadlem1  21140  lgsquad2lem1  21144  lgsquad3  21147  m1lgs  21148  2sqlem7  21156  chebbnd1lem2  21166  chebbnd1lem3  21167  rplogsumlem1  21180  rpvmasumlem  21183  dchrvmasumlem1  21191  dchrvmasum2lem  21192  dchrvmasumlema  21196  dchrisum0flblem2  21205  dchrisum0fno1  21207  dchrisum0re  21209  logdivsum  21229  pntrsumbnd2  21263  pntpbnd1a  21281  pntpbnd1  21282  pntibndlem2  21287  pntlemr  21298  pntlemj  21299  pntlemf  21301  pnt2  21309  padicabv  21326  ostth2lem2  21330  usgraidx2v  21414  iseupa  21689  eupap1  21700  eupath2lem3  21703  nmobndi  22278  ubthlem2  22375  ubthlem3  22376  minvecolem2  22379  shuni  22804  pjhthlem1  22895  chscllem2  23142  pjcompi  23176  mayete3i  23232  mayete3iOLD  23233  unoplin  23425  hmoplin  23447  nmophmi  23536  mdslmd4i  23838  preqsnd  24002  isoun  24091  xrofsup  24128  eliccelico  24142  elicoelioo  24143  difioo  24147  rexdiv  24174  xrge0addgt0  24216  ofldchr  24246  unitdivcld  24301  xrge0mulc1cn  24329  qqhnm  24376  esumcst  24457  esumfsup  24462  esumpmono  24471  esumcvg  24478  difelsiga  24518  1stmbfm  24612  2ndmbfm  24613  dya2icoseg  24629  probmeasb  24690  orvcgteel  24727  orvclteel  24732  ballotlemsima  24775  ballotlemfrceq  24788  lgamucov  24824  lgamcvg2  24841  subfacp1lem2a  24868  subfaclim  24876  erdsze2lem2  24892  cvmliftlem2  24975  cvmliftlem10  24983  cvmliftlem13  24985  cvmliftiota  24990  cvmlift2lem9  25000  cvmlift2lem11  25002  cvmlift2lem12  25003  cvmliftphtlem  25006  cvmlift3lem6  25013  cvmlift3lem7  25014  cvmlift3lem9  25016  snmlff  25018  mulge0b  25193  fprodser  25277  fprodshft  25302  fprodrev  25303  rprisefaccl  25341  trpredelss  25512  trpredpo  25515  wzel  25577  wsuclem  25578  nodenselem5  25642  nobndlem6  25654  brbtwn2  25846  colinearalglem2  25848  axcgrtr  25856  axcgrid  25857  axsegconlem7  25864  axsegcon  25868  ax5seglem3  25872  ax5seglem6  25875  ax5seg  25879  axpaschlem  25881  axlowdimlem17  25899  axcontlem2  25906  axcontlem4  25908  axcontlem7  25911  axcontlem8  25912  brsegle  26044  opnmbllem0  26244  mblfinlem3  26247  mblfinlem4  26248  itg2addnclem  26258  itg2addnc  26261  itg2gt0cn  26262  ftc1cnnclem  26280  ftc1cnnc  26281  areacirclem5  26298  opnregcld  26335  indexdom  26438  sstotbnd2  26485  isbnd3  26495  isbnd3b  26496  cntotbnd  26507  ismtyima  26514  heibor1lem  26520  heiborlem8  26529  rrncmslem  26543  reheibor  26550  lcomfsup  26749  mzpsubst  26807  eldioph2lem1  26820  eldioph2lem2  26821  eldioph2b  26823  diophin  26833  irrapxlem2  26888  irrapxlem4  26890  irrapxlem5  26891  pellexlem1  26894  pellexlem2  26895  pellexlem6  26899  elpell1qr2  26937  pell1qrgaplem  26938  pell1qrgap  26939  pellqrex  26944  pellfundex  26951  pellfund14  26963  rmspecsqrnq  26971  rmxyadd  26986  expmordi  27012  rmxypos  27014  jm2.24  27030  congsub  27037  mzpcong  27039  congrep  27040  acongtr  27045  acongrep  27047  jm2.19lem1  27062  jm2.22  27068  jm2.23  27069  jm2.26lem3  27074  jm2.26  27075  jm2.27a  27078  fnwe2lem2  27128  aomclem6  27136  frlmvscaval  27210  frlmssuvc1  27225  frlmsslsp  27227  frlmup1  27229  frlmup2  27230  enfixsn  27236  lindfind2  27267  lindfrn  27270  f1lindf  27271  islindf4  27287  hbtlem2  27307  hbtlem4  27309  hbtlem5  27311  dgraa0p  27333  rngunsnply  27357  pmtrff1o  27383  pmtrfcnv  27384  pmtrfb  27385  psgnunilem1  27395  mamudi  27440  mamudir  27441  acsfn1p  27486  proot1hash  27498  expgrowth  27531  itgsinexplem1  27726  stoweidlem11  27738  stoweidlem26  27753  stoweidlem34  27761  stoweidlem36  27763  stoweidlem38  27765  stirlinglem5  27805  cshw1  28297  lkrlsp  29962  lshpkrlem5  29974  ldualssvscl  30018  ldualssvsubcl  30019  llnmlplnN  30398  llncvrlpln  30417  pmapjat1  30712  pclfinN  30759  lautlt  30950  lauteq  30954  lautco  30956  ltrn11  30985  ltrnle  30988  ltrneq2  31007  cdlemednuN  31159  cdleme20k  31178  cdleme20l2  31180  cdleme20l  31181  cdleme20m  31182  cdleme21c  31186  cdleme22e  31203  cdleme22eALTN  31204  cdlemefrs32fva  31259  cdlemg4g  31475  cdlemg18b  31538  cdlemg18c  31539  cdlemj3  31682  dia2dimlem5  31928  dvhopN  31976  cdlemm10N  31978  dihjatcclem4  32281  dochexmidlem2  32321  lclkrlem2o  32381  lcfrlem5  32406  lcfrlem6  32407  lcdlssvscl  32466  mapdpglem6  32538  mapdpglem9  32540  mapdpglem12  32543  mapdpglem14  32545  mapdindp0  32579  hdmaprnlem7N  32718  hdmaprnlem8N  32719  hdmaprnlem3eN  32721  hgmapvvlem3  32788
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 179  df-an 362
  Copyright terms: Public domain W3C validator