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

Theorem syl22anc 1212
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 529 . 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 1209 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  4685  soltmin  5225  f1oprg  5669  fveqf1o  5987  weniso  6032  fr3nr  6380  smogt  6814  smorndom  6815  oacomf1o  6992  th3qlem1  7194  difsnen  7381  undom  7387  enfixsn  7408  domss2  7458  ssenen  7473  marypha1lem  7671  fisupcl  7705  ordtypelem3  7722  ordtypelem8  7727  oieu  7741  oismo  7742  wofib  7747  wemaplem2  7749  wemapso  7753  wemapso2OLD  7754  wemapso2lem  7755  unxpwdom2  7791  infdifsn  7850  oemapvali  7880  cantnflem1c  7883  cantnflem1d  7884  cantnflem1  7885  cantnf  7889  cantnfOLD  7911  cnfcom3  7925  cnfcom3OLD  7933  r1ordg  7973  dif1card  8165  infxpenlem  8168  dfac8clem  8190  infxp  8372  infmap2  8375  cflim2  8420  coftr  8430  fin2i2  8475  enfin2i  8478  fin23lem26  8482  fin23lem27  8485  fin23lem40  8508  isf32lem2  8511  isf32lem3  8512  isf32lem4  8513  isf32lem7  8516  isf32lem9  8518  fin1a2lem13  8569  fin12  8570  alephexp1  8731  gchdomtri  8784  fpwwe2lem12  8796  fpwwe2lem13  8797  gchpwdom  8825  gchhar  8834  adderpqlem  9111  mulerpqlem  9112  addassnq  9115  mulassnq  9116  distrnq  9118  mulidnq  9120  recmulnq  9121  ltexnq  9132  distrlem1pr  9182  distrlem4pr  9183  prlem936  9204  reclem3pr  9206  mulgt0d  9514  mul4d  9569  add4d  9581  add42d  9582  subcan  9652  addsub4d  9754  subadd4d  9755  sub4d  9756  2addsubd  9757  addsubeq4d  9758  muladdd  9790  mulsubd  9791  addgegt0d  9901  addge0d  9903  mulge0d  9904  le2addd  9945  le2subd  9946  ltleaddd  9947  leltaddd  9948  lt2subd  9950  divdivdiv  10020  divcan5  10021  divne0d  10111  recdivd  10112  recdiv2d  10113  divcan6d  10114  ddcand  10115  rec11d  10116  divmuldivd  10136  divmul13d  10137  divmul24d  10138  divadddivd  10139  divsubdivd  10140  divmuleqd  10141  divdivdivd  10142  subrecd  10150  mulge0b  10187  recreclt  10219  divgt0d  10256  mulgt1d  10257  lemulge11d  10258  lemulge12d  10259  ltmul12ad  10262  lemul12ad  10263  lemul12bd  10264  supmul1  10283  nndivtr  10351  qreccl  10961  ledivdivd  11040  lediv12ad  11070  lt2mul2divd  11073  xlt2add  11211  supxrun  11266  supxrre  11278  infmxrre  11286  iccss2  11354  iccssico2  11357  lincmb01cmp  11415  iccf1o  11416  fzrev2i  11505  modaddmodup  11746  modaddmodlo  11747  modsubdir  11751  fzennn  11774  sermono  11822  mulexpz  11888  expaddz  11892  ltexp2a  11899  leexp2a  11903  sqdiv  11915  expmulnbnd  11980  digit1  11982  expsubd  12003  lt2sqd  12026  le2sqd  12027  sq11d  12028  bcm1k  12075  bcp1n  12076  bcp1nk  12077  hashf1lem1  12192  cshw1  12440  2swrd2eqwrdeq  12537  absrele  12781  sqreulem  12831  sqrmuld  12895  sqrsq2d  12896  sqrled  12897  sqrltd  12898  sqr11d  12899  abs3lemd  12931  rlimuni  13012  climuni  13014  lo1resb  13026  o1resb  13028  2clim  13034  addcn2  13055  mulcn2  13057  o1of2  13074  o1rlimmul  13080  lo1add  13088  lo1mul  13089  isercolllem1  13126  caucvgrlem  13134  iseraltlem2  13144  iseraltlem3  13145  iseralt  13146  fsumrev  13229  fsumshft  13230  fsum0diag2  13233  binomlem  13275  climcndslem1  13295  climcndslem2  13296  harmonic  13304  mertenslem1  13327  efcllem  13346  moddvds  13525  dvds1  13564  dvdsext  13567  oexpneg  13578  bitsinv1  13621  sadaddlem  13645  sadasslem  13649  sadeq  13651  mulgcd  13713  dvdssqlem  13726  rpmulgcd2  13774  isprm6  13778  isprm5  13781  crt  13836  eulerthlem2  13840  prmdiveq  13844  pythagtriplem11  13875  pythagtriplem13  13877  iserodd  13885  pcgcd1  13926  pcprmpw2  13931  pcaddlem  13933  fldivp1  13942  4sqlem12  14000  4sqlem14  14002  4sqlem15  14003  4sqlem16  14004  vdwapun  14018  mreexexlem4d  14568  acsfn1  14582  acsfn2  14584  sscpwex  14711  rescabs  14729  catciso  14958  yonedainv  15074  subm0  15466  pmtrff1o  15949  pmtrfcnv  15950  pmtrfb  15951  psgnunilem1  15979  odmodnn0  16023  odeq  16033  dfod2  16045  sylow1lem1  16077  lsmsubg  16133  lsmmod  16152  lsmdisj2  16159  ghmplusg  16308  odadd  16312  gexexlem  16314  lt6abl  16351  cyggex2  16353  dprdfinv  16483  dmdprdsplitlem  16508  dpjidcl  16531  ablfacrp  16541  ablfacrp2  16542  ablfac1c  16546  ablfac1eu  16548  lcomfsupOLD  16908  lcomfsupp  16909  lssvancl1  16948  lssvnegcl  16959  lspprvacl  17002  lspsneli  17004  lspsn  17005  lmhmplusg  17047  lmhmima  17050  lmhmpreima  17051  reslmhm  17055  lbsind2  17084  lsmcl  17086  lsmelval2  17088  lsppreli  17093  lspprabs  17098  pj1lmhm  17103  lssvs0or  17113  lspabs3  17124  lspfixed  17131  lspexch  17132  lsmcv  17144  lspsolv  17146  lidlmcl  17221  drngnidl  17233  2idlcpbl  17238  mplbas2  17483  mplbas2OLD  17484  coe1addfv  17617  gzrngunit  17722  zringlpirlem3  17747  zlpirlem3  17752  prmirredlem  17759  prmirredlemOLD  17762  znf1o  17826  znunithash  17839  evpmodpmf1o  17868  frlmsubgval  18034  frlmvscaval  18036  frlmphllem  18047  frlmphl  18048  frlmssuvc1  18061  frlmssuvc1OLD  18063  frlmsslsp  18065  frlmsslspOLD  18066  frlmup1  18068  frlmup2  18069  lindfind2  18089  lindfrn  18092  f1lindf  18093  islindf4  18109  mamudi  18149  mamudir  18150  1marepvmarrepid  18228  mdetrlin  18251  smadiadetglem1  18319  smadiadetg  18321  cramerimplem1  18331  ntrin  18507  topssnei  18570  restbas  18604  restntr  18628  cnntri  18717  fiuncmp  18849  nllyrest  18932  nllyidm  18935  hausllycmp  18940  cldllycmp  18941  hauspwdom  18947  txcld  19018  txcn  19041  txlly  19051  txnlly  19052  txhaus  19062  txlm  19063  txkgen  19067  xkococnlem  19074  cnmpt2res  19092  xkoinjcn  19102  basqtop  19126  qtopeu  19131  qtophmeo  19232  trfbas2  19258  neifil  19295  hausflim  19396  alexsubALTlem2  19462  cnextfval  19476  cnextfvval  19479  cnextf  19480  clssubg  19521  utop2nei  19667  utop3cls  19668  utopreg  19669  psmetlecl  19733  xmetlecl  19763  prdsxmetlem  19785  bldisj  19815  imasf1obl  19905  prdsbl  19908  stdbdmet  19933  stdbdmopn  19935  met2ndci  19939  metcnp  19958  metusttoOLD  19974  metustto  19975  metustexhalfOLD  19980  metustexhalf  19981  cfilucfilOLD  19986  cfilucfil  19987  metucnOLD  20005  metucn  20006  lssnlm  20123  nmotri  20160  nmoid  20163  tgioo  20215  blcvx  20217  xrsmopn  20231  reperflem  20237  reconnlem2  20246  opnreen  20250  metdsge  20267  metdsre  20271  metdscnlem  20273  metnrmlem1a  20276  metnrmlem1  20277  metnrmlem3  20279  cncfmet  20326  cnmpt2pc  20342  icopnfcnv  20356  icopnfhmeo  20357  cnllycmp  20370  evth  20373  lebnumii  20380  nmoleub2lem3  20512  iscfil2  20619  cfil3i  20622  iscfil3  20626  cfilfcls  20627  iscau3  20631  iscmet3lem2  20645  caubl  20660  lmcau  20665  rrxcph  20738  minveclem2  20755  pjthlem1  20766  pjthlem2  20767  ivthicc  20784  ovollecl  20808  ovolunlem1a  20821  ovolunnul  20825  ovoliunlem1  20827  ismbl2  20852  nulmbl2  20860  unmbl  20861  volun  20868  voliunlem2  20874  ioombl1lem2  20882  uniioombllem2a  20904  uniioombllem3  20907  uniioombllem4  20908  dyaddisjlem  20917  dyadmaxlem  20919  opnmbllem  20923  volsup2  20927  volcn  20928  ismbfd  20960  mbfi1fseqlem1  21035  mbfi1fseqlem5  21039  itg2lecl  21058  itg2monolem2  21071  itg2gt0  21080  itgspliticc  21156  ellimc3  21196  limcres  21203  dvfval  21214  dvres3  21230  dvres3a  21231  dvnff  21239  dvnadd  21245  dvn2bss  21246  dvnres  21247  dvcmul  21260  dvcmulf  21261  dvmptres3  21272  dvmptres2  21278  dvmptntr  21287  dvexp3  21292  dvferm1lem  21298  dvlip  21307  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  dvgt0lem1  21316  dvgt0lem2  21317  dvne0  21325  lhop1lem  21327  lhop2  21329  lhop  21330  dvcnvrelem1  21331  dvcnvrelem2  21332  dvcvx  21334  dvfsumle  21335  dvfsumabs  21337  dvfsumlem2  21341  ftc1lem6  21355  ftc1  21356  ftc2ditglem  21359  itgsubstlem  21362  evlslem3  21366  evlslem1  21367  evl1addd  21385  evl1subd  21386  evl1muld  21387  tdeglem4  21414  mdegaddle  21430  mdegmullem  21434  ply1rem  21520  fta1glem2  21523  fta1blem  21525  ig1peu  21528  ig1pdvds  21533  dgrmulc  21623  dgrcolem1  21625  plydivlem4  21647  plydiveu  21649  fta1lem  21658  vieta1lem1  21661  vieta1lem2  21662  plyexmo  21664  taylfvallem1  21707  taylfval  21709  tayl0  21712  taylplem1  21713  taylply2  21718  taylply  21719  dvtaylp  21720  dvntaylp  21721  dvntaylp0  21722  taylthlem1  21723  taylthlem2  21724  ulmcaulem  21744  ulmcau  21745  ulmcn  21749  ulmdvlem1  21750  radcnvlem1  21763  radcnvle  21770  psercn  21776  pserdvlem2  21778  pserdv  21779  abelth  21791  cosordlem  21872  tanregt0  21880  dvlog2lem  21982  efopn  21988  logtayllem  21989  logccv  21993  cxplt3  22030  cxpmul2zd  22046  cxpltd  22049  cxpled  22050  cxplt3d  22062  cxple3d  22063  dvsqr  22067  cxpcn3  22071  cxpaddle  22075  cxpeq  22080  angcan  22083  angvald  22085  ang180lem2  22091  ang180  22095  isosctrlem3  22103  dquartlem1  22131  atantayl2  22218  leibpilem1  22220  leibpi  22222  log2tlbnd  22225  birthdaylem3  22232  xrlimcnp  22247  efrlim  22248  o1cxp  22253  jensenlem2  22266  jensen  22267  fsumharmonic  22290  wilthlem1  22291  basellem3  22305  basellem6  22308  basellem8  22310  ppisval  22326  chtwordi  22379  ppiwordi  22385  mumullem2  22403  dvdsmulf1o  22419  fsumvma  22437  fsumvma2  22438  chpchtsum  22443  chpub  22444  logfacubnd  22445  dchrmulcl  22473  dchrinv  22485  dchrptlem1  22488  dchrptlem2  22489  sumdchr2  22494  dchr2sum  22497  bposlem7  22514  lgslem1  22520  lgslem3  22522  lgsdirprm  22553  lgsqrlem2  22566  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem4  22576  lgseisen  22577  lgsquadlem1  22578  lgsquad2lem1  22582  lgsquad3  22585  m1lgs  22586  2sqlem7  22594  chebbnd1lem2  22604  chebbnd1lem3  22605  rplogsumlem1  22618  rpvmasumlem  22621  dchrvmasumlem1  22629  dchrvmasum2lem  22630  dchrvmasumlema  22634  dchrisum0flblem2  22643  dchrisum0fno1  22645  dchrisum0re  22647  logdivsum  22667  pntrsumbnd2  22701  pntpbnd1a  22719  pntpbnd1  22720  pntibndlem2  22725  pntlemr  22736  pntlemj  22737  pntlemf  22739  pnt2  22747  padicabv  22764  ostth2lem2  22768  f1otrg  22940  brbtwn2  22974  colinearalglem2  22976  axcgrtr  22984  axcgrid  22985  axsegconlem7  22992  axsegcon  22996  ax5seglem3  23000  ax5seglem6  23003  ax5seg  23007  axpaschlem  23009  axlowdimlem17  23027  axcontlem2  23034  axcontlem4  23036  axcontlem7  23039  axcontlem8  23040  ecgrtg  23052  usgraidx2v  23134  iseupa  23409  eupap1  23420  eupath2lem3  23423  nmobndi  23998  ubthlem2  24095  ubthlem3  24096  minvecolem2  24099  shuni  24526  pjhthlem1  24617  chscllem2  24864  pjcompi  24898  mayete3i  24954  mayete3iOLD  24955  unoplin  25147  hmoplin  25169  nmophmi  25258  mdslmd4i  25560  preqsnd  25725  isoun  25821  xrofsup  25878  eliccelico  25890  elicoelioo  25891  difioo  25895  rexdiv  25924  xrge0addgt0  25977  omndadd2d  25995  omndadd2rd  25996  unitdivcld  26185  xrge0mulc1cn  26225  qqhnm  26273  esumcst  26368  esumfsup  26373  esumpmono  26382  esumcvg  26389  difelsiga  26430  1stmbfm  26529  2ndmbfm  26530  dya2icoseg  26546  sibfinima  26573  probmeasb  26661  orvcgteel  26698  orvclteel  26703  ballotlemsima  26746  ballotlemfrceq  26759  sgnmul  26773  ccatmulgnn0dir  26788  ofccat  26789  lgamucov  26872  lgamcvg2  26889  subfacp1lem2a  26916  subfaclim  26924  erdsze2lem2  26940  cvmliftlem2  27023  cvmliftlem10  27031  cvmliftlem13  27033  cvmliftiota  27038  cvmlift2lem9  27048  cvmlift2lem11  27050  cvmlift2lem12  27051  cvmliftphtlem  27054  cvmlift3lem6  27061  cvmlift3lem7  27062  cvmlift3lem9  27064  snmlff  27066  fprodser  27309  fprodshft  27334  fprodrev  27335  rprisefaccl  27373  trpredelss  27543  trpredpo  27546  wzel  27608  wsuclem  27609  nodenselem5  27673  nobndlem6  27685  brsegle  27986  fin2so  28260  opnmbllem0  28271  mblfinlem3  28274  mblfinlem4  28275  itg2addnclem  28287  itg2addnc  28290  itg2gt0cn  28291  ftc1cnnclem  28309  ftc1cnnc  28310  areacirclem5  28332  opnregcld  28369  indexdom  28472  sstotbnd2  28517  isbnd3  28527  isbnd3b  28528  cntotbnd  28539  ismtyima  28546  heibor1lem  28552  heiborlem8  28561  rrncmslem  28575  reheibor  28582  mzpsubst  28930  eldioph2lem1  28943  eldioph2lem2  28944  eldioph2b  28946  diophin  28956  irrapxlem2  29009  irrapxlem4  29011  irrapxlem5  29012  pellexlem1  29015  pellexlem2  29016  pellexlem6  29020  elpell1qr2  29058  pell1qrgaplem  29059  pell1qrgap  29060  pellqrex  29065  pellfundex  29072  pellfund14  29084  rmspecsqrnq  29092  rmxyadd  29107  expmordi  29133  rmxypos  29135  jm2.24  29151  congsub  29158  mzpcong  29160  congrep  29161  acongtr  29166  acongrep  29168  jm2.19lem1  29183  jm2.22  29189  jm2.23  29190  jm2.26lem3  29195  jm2.26  29196  jm2.27a  29199  fnwe2lem2  29249  aomclem6  29257  hbtlem2  29325  hbtlem4  29327  hbtlem5  29329  dgraa0p  29351  rngunsnply  29375  acsfn1p  29401  proot1hash  29413  itgpowd  29435  expgrowth  29454  itgsinexplem1  29640  stoweidlem11  29652  stoweidlem26  29667  stoweidlem34  29675  stoweidlem36  29677  stoweidlem38  29679  stirlinglem5  29719  numclwwlkovf2ex  30525  lkrlsp  32320  lshpkrlem5  32332  ldualssvscl  32376  ldualssvsubcl  32377  llnmlplnN  32756  llncvrlpln  32775  pmapjat1  33070  pclfinN  33117  lautlt  33308  lauteq  33312  lautco  33314  ltrn11  33343  ltrnle  33346  ltrneq2  33365  cdlemednuN  33517  cdleme20k  33536  cdleme20l2  33538  cdleme20l  33539  cdleme20m  33540  cdleme21c  33544  cdleme22e  33561  cdleme22eALTN  33562  cdlemefrs32fva  33617  cdlemg4g  33833  cdlemg18b  33896  cdlemg18c  33897  cdlemj3  34040  dia2dimlem5  34286  dvhopN  34334  cdlemm10N  34336  dihjatcclem4  34639  dochexmidlem2  34679  lclkrlem2o  34739  lcfrlem5  34764  lcfrlem6  34765  lcdlssvscl  34824  mapdpglem6  34896  mapdpglem9  34898  mapdpglem12  34901  mapdpglem14  34903  mapdindp0  34937  hdmaprnlem7N  35076  hdmaprnlem8N  35077  hdmaprnlem3eN  35079  hgmapvvlem3  35146
  Copyright terms: Public domain W3C validator