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

Theorem syl22anc 1277
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 539 . 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 1274 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  preqsnd  4171  fr2nr  4830  soltmin  5254  f1oprg  5877  f1prex  6206  fveqf1o  6224  weniso  6269  fr3nr  6632  smogt  7111  smorndom  7112  oacomf1o  7291  difsnen  7679  undom  7685  enfixsn  7706  domss2  7756  ssenen  7771  marypha1lem  7972  fisupcl  8010  ordtypelem3  8060  ordtypelem8  8065  oieu  8079  oismo  8080  wofib  8085  wemaplem2  8087  wemapso  8091  wemapso2lem  8092  unxpwdom2  8128  infdifsn  8187  oemapvali  8214  cantnflem1c  8217  cantnflem1  8219  cantnf  8223  cnfcom3  8234  r1ordg  8274  dif1card  8466  infxpenlem  8469  dfac8clem  8488  infxp  8670  infmap2  8673  cflim2  8718  coftr  8728  fin2i2  8773  enfin2i  8776  fin23lem26  8780  fin23lem27  8783  fin23lem40  8806  isf32lem2  8809  isf32lem3  8810  isf32lem4  8811  isf32lem7  8814  isf32lem9  8816  fin1a2lem13  8867  fin12  8868  alephexp1  9029  gchdomtri  9079  fpwwe2lem12  9091  fpwwe2lem13  9092  gchpwdom  9120  gchhar  9129  adderpqlem  9404  mulerpqlem  9405  addassnq  9408  mulassnq  9409  distrnq  9411  mulidnq  9413  recmulnq  9414  ltexnq  9425  distrlem1pr  9475  distrlem4pr  9476  prlem936  9497  reclem3pr  9499  mulcmpblnr  9520  mulgt0d  9815  mul4d  9870  add4d  9883  add42d  9884  subcan  9954  addsub4d  10058  subadd4d  10059  sub4d  10060  2addsubd  10061  addsubeq4d  10062  muladdd  10103  mulsubd  10104  addgegt0d  10214  addge0d  10216  mulge0d  10217  le2addd  10259  le2subd  10260  ltleaddd  10261  leltaddd  10262  lt2subd  10264  divdivdiv  10335  divcan5  10336  divne0d  10426  recdivd  10427  recdiv2d  10428  divcan6d  10429  ddcand  10430  rec11d  10431  divmuldivd  10451  divmul13d  10452  divmul24d  10453  divadddivd  10454  divsubdivd  10455  divmuleqd  10456  divdivdivd  10457  subrecd  10465  mulge0b  10502  recreclt  10532  divgt0d  10569  mulgt1d  10570  lemulge11d  10571  lemulge12d  10572  ltmul12ad  10575  lemul12ad  10576  lemul12bd  10577  supmul1  10603  nndivtr  10678  qreccl  11312  ledivdivd  11394  lediv12ad  11425  lt2mul2divd  11433  xlt2add  11574  supxrun  11629  supxrre  11641  infxrre  11650  infmxrreOLD  11654  elicore  11715  iccss2  11733  iccssico2  11736  lincmb01cmp  11803  iccf1o  11804  fzrev2i  11888  fz1fzo0m1  11993  modaddmodup  12184  modaddmodlo  12185  modsubdir  12189  fzennn  12212  sermono  12276  mulexpz  12343  expaddz  12347  ltexp2a  12355  leexp2a  12359  sqdiv  12371  expmulnbnd  12435  digit1  12437  expsubd  12458  lt2sqd  12481  le2sqd  12482  sq11d  12483  bcm1k  12531  bcp1n  12532  bcp1nk  12533  hashf1lem1  12650  cshw1  12957  2swrd2eqwrdeq  13076  absrele  13419  sqreulem  13470  sqrtmuld  13534  sqrtsq2d  13535  sqrtled  13536  sqrtltd  13537  sqr11d  13538  abs3lemd  13571  rlimuni  13662  climuni  13664  lo1resb  13676  o1resb  13678  2clim  13684  addcn2  13705  mulcn2  13707  o1of2  13724  o1rlimmul  13730  lo1add  13738  lo1mul  13739  isercolllem1  13776  caucvgrlem  13784  caucvgrlemOLD  13785  iseraltlem2  13797  iseraltlem3  13798  iseralt  13799  mptfzshft  13887  fsumrev  13888  fsum0diag2  13892  binomlem  13935  climcndslem1  13955  climcndslem2  13956  harmonic  13965  mertenslem1  13988  fprodser  14051  fprodrev  14079  rprisefaccl  14124  efcllem  14180  moddvds  14360  dvds1  14401  dvdsext  14404  oexpneg  14416  bitsinv1  14464  sadaddlem  14488  sadasslem  14492  sadeq  14494  mulgcd  14562  dvdssqlem  14575  lcmftp  14657  isprm5  14699  rpmulgcd2  14710  isprm6  14714  coprmproddvdslem  14727  crt  14774  eulerthlem2  14778  prmdiveq  14782  pythagtriplem11  14823  pythagtriplem13  14825  iserodd  14833  pcgcd1  14874  pcprmpw2  14879  pcaddlem  14881  fldivp1  14890  4sqlem12  14948  4sqlem14OLD  14950  4sqlem15OLD  14951  4sqlem16OLD  14952  4sqlem14  14956  4sqlem15  14957  4sqlem16  14958  vdwapun  14972  mreexexlem4d  15601  acsfn1  15615  acsfn2  15617  sscpwex  15768  rescabs  15786  yonedainv  16214  subm0  16651  pmtrfb  17154  psgnunilem1  17182  odmodnn0  17237  odeq  17247  dfod2  17263  sylow1lem1  17298  lsmsubg  17354  lsmmod  17373  lsmdisj2  17380  ghmplusg  17532  odadd  17536  gexexlem  17538  lt6abl  17577  cyggex2  17579  dprdfinv  17700  dmdprdsplitlem  17718  dpjidcl  17739  ablfacrp  17747  ablfacrp2  17748  ablfac1c  17752  ablfac1eu  17754  lcomfsupp  18176  lssvancl1  18216  lssvnegcl  18227  lspprvacl  18270  lspsneli  18272  lspsn  18273  lmhmplusg  18315  lmhmima  18318  lmhmpreima  18319  reslmhm  18323  lbsind2  18352  lsmcl  18354  lsmelval2  18356  lsppreli  18361  lspprabs  18366  pj1lmhm  18371  lssvs0or  18381  lspabs3  18392  lspfixed  18399  lspexch  18400  lsmcv  18412  lspsolv  18414  lidlmcl  18489  drngnidl  18501  2idlcpbl  18506  mplbas2  18742  evlslem3  18785  evlslem1  18786  coe1addfv  18906  lply1binom  18948  evl1addd  18977  evl1subd  18978  evl1muld  18979  gzrngunit  19081  zringlpirlem3OLD  19103  zringlpirlem3  19105  prmirredlem  19112  znf1o  19170  znunithash  19183  frlmsubgval  19375  frlmvscaval  19377  frlmphllem  19386  frlmphl  19387  frlmssuvc1  19400  frlmsslsp  19402  frlmup1  19404  frlmup2  19405  lindfind2  19424  lindfrn  19427  f1lindf  19428  islindf4  19444  mamudi  19476  mamudir  19477  1marepvmarrepid  19648  mdetrlin  19675  smadiadetglem1  19744  smadiadetg  19746  cramerimplem1  19756  mat2pmatscmxcl  19812  m2pmfzgsumcl  19820  pmatcollpw  19853  pmatcollpwfi  19854  pmatcollpw3fi1lem1  19858  cpmidpmatlem2  19943  cpmadugsumlemF  19948  chcoeffeqlem  19957  ntrin  20124  topssnei  20188  restbas  20222  restntr  20246  cnntri  20335  fiuncmp  20467  nllyrest  20549  nllyidm  20552  hausllycmp  20557  cldllycmp  20558  hauspwdom  20564  txcld  20666  txcn  20689  txlly  20699  txnlly  20700  txhaus  20710  txlm  20711  txkgen  20715  xkococnlem  20722  cnmpt2res  20740  xkoinjcn  20750  basqtop  20774  qtopeu  20779  trfbas2  20906  neifil  20943  hausflim  21044  alexsubALTlem2  21111  cnextfval  21125  cnextfvval  21128  cnextf  21129  cnextfres  21132  clssubg  21171  utop2nei  21313  utop3cls  21314  utopreg  21315  psmetlecl  21379  xmetlecl  21409  prdsxmetlem  21431  bldisj  21461  imasf1obl  21551  prdsbl  21554  stdbdmet  21579  stdbdmopn  21581  met2ndci  21585  metcnp  21604  metustto  21616  metustexhalf  21619  cfilucfil  21622  metucn  21634  lssnlm  21751  nmotri  21808  nmoid  21811  tgioo  21862  blcvx  21864  xrsmopn  21878  reperflem  21884  reconnlem2  21893  opnreen  21897  metdsge  21914  metdsre  21918  metdscnlem  21920  metnrmlem1a  21923  metnrmlem1  21924  metnrmlem3  21926  metdsgeOLD  21929  metdsreOLD  21933  metdscnlemOLD  21935  metnrmlem1aOLD  21938  metnrmlem1OLD  21939  metnrmlem3OLD  21941  cncfmet  21988  cnmpt2pc  22004  icopnfcnv  22018  icopnfhmeo  22019  cnllycmp  22032  evth  22035  lebnumii  22045  nmoleub2lem3  22177  iscfil2  22284  cfil3i  22287  iscfil3  22291  cfilfcls  22292  iscau3  22296  iscmet3lem2  22310  caubl  22325  lmcau  22330  rrxcph  22399  minveclem2  22416  minveclem2OLD  22428  pjthlem1  22439  pjthlem2  22440  ivthicc  22457  ovollecl  22484  ovolunlem1a  22497  ovolunnul  22501  ovoliunlem1  22503  ismbl2  22529  nulmbl2  22538  unmbl  22539  volun  22546  voliunlem2  22552  ioombl1lem2  22560  uniioombllem2a  22587  uniioombllem3  22591  uniioombllem4  22592  dyaddisjlem  22601  dyadmaxlem  22603  opnmbllem  22607  volsup2  22611  volcn  22612  ismbfd  22644  mbfi1fseqlem1  22721  mbfi1fseqlem5  22725  itg2lecl  22744  itg2monolem2  22757  itg2gt0  22766  itgspliticc  22842  ellimc3  22882  limcres  22889  dvfval  22900  dvres3  22916  dvres3a  22917  dvnff  22925  dvnadd  22931  dvn2bss  22932  dvnres  22933  dvcmul  22946  dvcmulf  22947  dvmptres3  22958  dvmptres2  22964  dvmptntr  22973  dvexp3  22978  dvferm1lem  22984  dvlip  22993  dvlipcn  22994  dvlip2  22995  c1liplem1  22996  dvgt0lem1  23002  dvgt0lem2  23003  dvne0  23011  lhop1lem  23013  lhop2  23015  lhop  23016  dvcnvrelem1  23017  dvcnvrelem2  23018  dvcvx  23020  dvfsumle  23021  dvfsumabs  23023  dvfsumlem2  23027  ftc1lem6  23041  ftc1  23042  ftc2ditglem  23045  itgsubstlem  23048  tdeglem4  23057  mdegaddle  23071  mdegmullem  23075  ply1rem  23162  fta1glem2  23165  fta1blem  23167  ig1peu  23170  ig1peuOLD  23171  ig1pdvds  23176  ig1pdvdsOLD  23182  dgrmulc  23273  dgrcolem1  23275  plydivlem4  23297  plydiveu  23299  fta1lem  23308  vieta1lem1  23311  vieta1lem2  23312  plyexmo  23314  taylfvallem1  23360  taylfval  23362  tayl0  23365  taylplem1  23366  taylply2  23371  taylply  23372  dvtaylp  23373  dvntaylp  23374  dvntaylp0  23375  taylthlem1  23376  taylthlem2  23377  ulmcaulem  23397  ulmcau  23398  ulmcn  23402  ulmdvlem1  23403  radcnvlem1  23416  radcnvle  23423  psercn  23429  pserdvlem2  23431  pserdv  23432  abelth  23444  cosordlem  23528  tanregt0  23536  dvlog2lem  23645  efopn  23651  logtayllem  23652  logccv  23656  cxplt3  23693  cxpmul2zd  23709  cxpltd  23712  cxpled  23713  cxplt3d  23725  cxple3d  23726  dvsqrt  23730  cxpcn3  23736  cxpaddle  23740  cxpeq  23745  angcan  23779  angvald  23781  ang180lem2  23787  ang180  23791  isosctrlem3  23797  dquartlem1  23825  atantayl2  23912  leibpilem1  23914  leibpi  23916  log2tlbnd  23919  birthdaylem3  23927  xrlimcnp  23942  efrlim  23943  o1cxp  23948  jensenlem2  23961  jensen  23962  fsumharmonic  23985  lgamucov  24011  lgamcvg2  24028  wilthlem1  24041  basellem3  24057  basellem6  24060  basellem8  24062  ppisval  24078  chtwordi  24131  ppiwordi  24137  mumullem2  24155  dvdsmulf1o  24171  fsumvma  24189  fsumvma2  24190  chpchtsum  24195  chpub  24196  logfacubnd  24197  dchrmulcl  24225  dchrinv  24237  dchrptlem1  24240  dchrptlem2  24241  sumdchr2  24246  dchr2sum  24249  bposlem7  24266  lgslem1  24272  lgslem3  24274  lgsdirprm  24305  lgsqrlem2  24318  lgseisenlem1  24325  lgseisenlem2  24326  lgseisenlem4  24328  lgseisen  24329  lgsquadlem1  24330  lgsquad2lem1  24334  lgsquad3  24337  m1lgs  24338  2sqlem7  24346  chebbnd1lem2  24356  chebbnd1lem3  24357  rplogsumlem1  24370  rpvmasumlem  24373  dchrvmasumlem1  24381  dchrvmasum2lem  24382  dchrvmasumlema  24386  dchrisum0flblem2  24395  dchrisum0fno1  24397  dchrisum0re  24399  logdivsum  24419  pntrsumbnd2  24453  pntpbnd1a  24471  pntpbnd1  24472  pntibndlem2  24477  pntlemr  24488  pntlemj  24489  pntlemf  24491  pnt2  24499  padicabv  24516  ostth2lem2  24520  f1otrg  24949  brbtwn2  24983  colinearalglem2  24985  axcgrtr  24993  axcgrid  24994  axsegconlem7  25001  axsegcon  25005  ax5seglem3  25009  ax5seglem6  25012  ax5seg  25016  axpaschlem  25018  axlowdimlem17  25036  axcontlem2  25043  axcontlem4  25045  axcontlem7  25048  axcontlem8  25049  ecgrtg  25061  usgraidx2v  25168  iseupa  25741  eupap1  25752  eupath2lem3  25755  numclwwlkovf2ex  25862  nmobndi  26464  ubthlem2  26561  ubthlem3  26562  minvecolem2  26565  minvecolem2OLD  26575  shuni  27001  pjhthlem1  27092  chscllem2  27339  pjcompi  27373  mayete3i  27429  unoplin  27621  hmoplin  27643  nmophmi  27732  mdslmd4i  28034  isoun  28330  xrge0addcld  28392  xrofsup  28401  eliccelico  28407  elicoelioo  28408  difioo  28412  rexdiv  28443  2sqmod  28457  xrge0addgt0  28502  omndadd2d  28519  omndadd2rd  28520  omndmul2  28523  ofldchr  28625  mdetpmtr2  28698  mdetpmtr12  28699  madjusmdetlem1  28701  madjusmdetlem4  28704  unitdivcld  28755  xrge0mulc1cn  28795  qqhnm  28842  esumcst  28932  esumfsup  28939  esumpmono  28948  esumcvg  28955  difelsiga  29003  sigapisys  29025  sigapildsys  29032  ldgenpisyslem1  29033  1stmbfm  29130  2ndmbfm  29131  dya2icoseg  29147  sibfinima  29220  probmeasb  29311  orvcgteel  29348  orvclteel  29353  ballotlemsima  29396  ballotlemfrceq  29409  ballotlemsimaOLD  29434  ballotlemfrceqOLD  29447  sgnmul  29461  ccatmulgnn0dir  29476  ofccat  29477  subfacp1lem2a  29951  subfaclim  29959  erdsze2lem2  29975  cvmliftlem2  30057  cvmliftlem10  30065  cvmliftlem13  30067  cvmliftiota  30072  cvmlift2lem9  30082  cvmlift2lem11  30084  cvmlift2lem12  30085  cvmliftphtlem  30088  cvmlift3lem6  30095  cvmlift3lem7  30096  cvmlift3lem9  30098  snmlff  30100  mrsubfval  30194  trpredelss  30521  trpredpo  30524  wzel  30555  wsuclem  30556  nodenselem5  30622  nobndlem6  30634  brsegle  30923  opnregcld  31034  fin2so  31976  poimirlem17  32001  poimirlem23  32007  opnmbllem0  32020  mblfinlem3  32023  mblfinlem4  32024  itg2addnclem  32037  itg2addnc  32040  itg2gt0cn  32041  ftc1cnnclem  32059  ftc1cnnc  32060  areacirclem5  32080  indexdom  32105  sstotbnd2  32150  isbnd3  32160  isbnd3b  32161  cntotbnd  32172  ismtyima  32179  heibor1lem  32185  heiborlem8  32194  rrncmslem  32208  reheibor  32215  lkrlsp  32712  lshpkrlem5  32724  ldualssvscl  32768  ldualssvsubcl  32769  llnmlplnN  33148  llncvrlpln  33167  pmapjat1  33462  pclfinN  33509  lautlt  33700  lauteq  33704  lautco  33706  ltrn11  33735  ltrnle  33738  ltrneq2  33757  cdlemednuN  33910  cdleme20k  33930  cdleme20l2  33932  cdleme20l  33933  cdleme20m  33934  cdleme21c  33938  cdleme22e  33955  cdleme22eALTN  33956  cdlemefrs32fva  34011  cdlemg4g  34227  cdlemg18b  34290  cdlemg18c  34291  cdlemj3  34434  dia2dimlem5  34680  dvhopN  34728  cdlemm10N  34730  dihjatcclem4  35033  dochexmidlem2  35073  lclkrlem2o  35133  lcfrlem5  35158  lcfrlem6  35159  lcdlssvscl  35218  mapdpglem6  35290  mapdpglem9  35292  mapdpglem12  35295  mapdpglem14  35297  mapdindp0  35331  hdmaprnlem7N  35470  hdmaprnlem8N  35471  hdmaprnlem3eN  35473  hgmapvvlem3  35540  mzpsubst  35634  eldioph2lem1  35646  eldioph2lem2  35647  eldioph2b  35649  diophin  35659  irrapxlem2  35711  irrapxlem4  35713  irrapxlem5  35714  pellexlem1  35717  pellexlem2  35718  pellexlem6  35722  elpell1qr2  35762  pell1qrgaplem  35763  pell1qrgap  35764  pellqrex  35770  pellfundex  35778  pellfund14  35790  rmspecsqrtnq  35798  rmxyadd  35813  expmordi  35839  rmxypos  35841  jm2.24  35857  congsub  35864  mzpcong  35866  congrep  35867  acongtr  35872  acongrep  35874  jm2.19lem1  35888  jm2.22  35894  jm2.23  35895  jm2.26lem3  35900  jm2.26  35901  jm2.27a  35904  fnwe2lem2  35953  aomclem6  35961  hbtlem2  36027  hbtlem4  36029  hbtlem5  36031  dgraa0p  36059  rngunsnply  36083  acsfn1p  36109  proot1hash  36121  itgpowd  36143  expgrowth  36727  abslt2sqd  37620  ioondisj2  37626  ioondisj1  37627  eliocre  37646  ioossioobi  37655  lptioo2  37748  limcresiooub  37760  cncfuni  37801  cncfiooicclem1  37808  cxpcncf2  37815  dvcnre  37823  dvresntr  37825  dvmptresicc  37828  dvresioo  37830  dvbdfbdioolem1  37837  dvnmptdivc  37850  dvnxpaek  37854  itgsinexplem1  37867  itgcoscmulx  37883  itgiccshift  37894  itgperiod  37895  stoweidlem11  37908  stoweidlem26  37923  stoweidlem34  37932  stoweidlem36  37934  stoweidlem38  37936  stirlinglem5  37977  dirkercncflem2  38003  dirkercncflem4  38005  fourierdlem20  38026  fourierdlem58  38065  fourierdlem72  38079  fourierdlem73  38080  fourierdlem74  38081  fourierdlem75  38082  fourierdlem76  38083  fourierdlem79  38086  fourierdlem80  38087  fourierdlem87  38094  fourierdlem94  38101  fourierdlem103  38110  fourierdlem104  38111  fourierdlem107  38114  fourierdlem113  38120  sqwvfoura  38129  sqwvfourb  38130  fourierswlem  38131  fouriersw  38132  etransclem46  38182  etransclem47  38183  rrndistlt  38196  sge0ssre  38276  hsphoidmvle2  38444  hsphoidmvle  38445  hoidmv1lelem1  38450  hoidmv1lelem2  38451  hoidmv1lelem3  38452  hoidmvlelem1  38454  hoidifhspdmvle  38479  hoiqssbllem2  38482  iccpartdisj  38788  m1expevenALTV  38814  oexpnegALTV  38843  tgoldbach  38948  usgredg2v  39353  uhgeq12d  39959  usgedgvadf1  39999  usgedgvadf1ALT  40002  nn0eo  40607  fdivpm  40626  refdivpm  40627  elbigolo1  40640  logbpw2m1  40650  fllog2  40651  dignn0flhalflem1  40698  dignn0flhalflem2  40699
  Copyright terms: Public domain W3C validator