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

Theorem ad2antrl 708
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad2antrl  |-  ( ( ch  /\  ( ph  /\ 
th ) )  ->  ps )

Proof of Theorem ad2antrl
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 451 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantl 452 1  |-  ( ( ch  /\  ( ph  /\ 
th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simprl  732  simprll  738  simprlr  739  fr2nr  4387  tz7.7  4434  reusv2lem4  4554  onint  4602  ordsucelsuc  4629  somin1  5095  elxp5  5177  soisores  5840  wemoiso  5871  wemoiso2  5872  sorpssi  6299  tz7.48lem  6469  oalimcl  6574  oeeui  6616  oaabs2  6659  omabs  6661  swoer  6704  0er  6711  pw2f1olem  6982  mapxpen  7043  mapunen  7046  unxpdomlem2  7084  unxpdomlem3  7085  findcard3  7116  isfinite2  7131  domunfican  7145  fodomfi  7151  fissuni  7176  fipreima  7177  indexfi  7179  marypha1lem  7202  marypha2  7208  supmo  7219  oieu  7270  brwdom2  7303  ixpiunwdom  7321  cantnfval2  7386  cantnfle  7388  cantnflt  7389  cantnf  7411  wemapwe  7416  cnfcom  7419  rankonidlem  7516  r1pwcl  7535  infxpenlem  7657  infxpenc2lem1  7662  fseqenlem1  7667  dfac8clem  7675  mappwen  7755  dfac3  7764  dfac5  7771  dfac12lem3  7787  cdainf  7834  infunsdom  7856  coftr  7915  ssfin4  7952  domfin4  7953  fin23lem26  7967  fin23lem22  7969  fin23lem28  7982  fin23lem32  7986  fin23lem40  7993  isf32lem5  7999  compssiso  8016  isf34lem4  8019  isfin1-3  8028  fin1a2lem13  8054  hsmexlem2  8069  hsmexlem4  8071  zorn2lem1  8139  ttukeylem6  8157  iundom2g  8178  konigthlem  8206  pwcfsdom  8221  fpwwe2lem12  8279  fpwwe2  8281  pwfseqlem3  8298  winalim2  8334  r1wunlim  8375  inttsk  8412  inar1  8413  grur1  8458  nqereq  8575  ltexprlem7  8682  prlem936  8687  00id  9003  addid2  9011  ltord1  9315  divdiv1  9487  divdiv2  9488  conjmul  9493  ltdivmul  9644  ledivmul  9645  lt2mul2div  9648  ltdiv23  9663  lediv23  9664  lediv12a  9665  ledivp1  9674  peano2uz2  10115  peano5uzi  10116  eluzp1m1  10267  qbtwnre  10542  xralrple  10548  xleadd1a  10589  xmulge0  10620  xmulass  10623  xlemul1a  10624  iooshf  10744  modadd1  11017  modmul1  11018  seqcl2  11080  seqfveq2  11084  seqid2  11108  seqhomo  11109  seqdistr  11113  mulexpz  11158  leexp2r  11175  expnlbnd2  11248  expmulnbnd  11249  hashmap  11403  hashfun  11405  hashbclem  11406  hashfacen  11408  hashf1lem2  11410  hashf1  11411  splid  11484  wrdind  11493  sqrlem1  11744  sqrlem6  11749  rlim  11985  rlimclim1  12035  climsup  12159  caurcvg2  12166  caucvgb  12168  iseralt  12173  sumss  12213  fsum2dlem  12249  fsumshft  12258  o1fsum  12287  incexclem  12311  divrcnv  12327  flo1  12329  ruclem6  12529  moddvds  12554  dvdseq  12592  bitsf1ocnv  12651  bitsf1  12653  sadcaddlem  12664  bezoutlem2  12734  bezoutlem4  12736  prmind2  12785  isprm6  12804  isprm5  12807  hashdvds  12859  crt  12862  eulerthlem2  12866  prmdiveq  12870  iserodd  12904  pclem  12907  pcprendvds2  12910  pcexp  12928  pcneg  12942  pc2dvds  12947  pcmpt  12956  prmpwdvds  12967  pockthg  12969  prmreclem5  12983  4sqlem11  13018  ramub2  13077  ramubcl  13081  ram0  13085  ramub1lem2  13090  ramcl  13092  setscom  13192  sscpwex  13708  setcinv  13938  1stfcl  13987  2ndfcl  13988  hofpropd  14057  isacs3lem  14285  isacs4lem  14287  acsmap2d  14298  submnd0  14418  subsubm  14450  frmdup1  14502  frmdup3  14504  isgrpinv  14548  subsubg  14656  cycsubgcl  14659  conjghm  14729  divsghm  14735  gsumwrev  14855  odf1o2  14900  sylow1lem1  14925  odcau  14931  pgpfi  14932  pgpssslw  14941  fislw  14952  efgtlen  15051  efginvrel2  15052  efgrelexlemb  15075  efgredeu  15077  efgcpbllemb  15080  frgpup1  15100  cygabl  15193  lt6abl  15197  gsum2d  15239  gsum2d2lem  15240  gsum2d2  15241  dmdprdsplit2lem  15296  ablfacrp  15317  pgpfac1lem3  15328  irredrmul  15505  subsubrg  15587  islss4  15735  lspextmo  15829  lspsnat  15914  issubassa  16080  resspsradd  16176  resspsrmul  16177  coe1tmmul2  16368  prmirredlem  16462  znf1o  16521  znidomb  16531  frgpcyg  16543  tgcl  16723  pptbas  16761  clsval2  16803  mretopd  16845  lmbr2  17005  cncls2  17018  nrmsep  17101  regsep2  17120  cmpsublem  17142  cmpsub  17143  tgcmp  17144  uncmp  17146  hauscmplem  17149  iunconlem  17169  1stcrest  17195  2ndcctbss  17197  2ndcsep  17201  dis2ndc  17202  hausllycmp  17236  dislly  17239  kgentopon  17249  1stckgen  17265  kgencn3  17269  ptpjpre1  17282  ptbasin  17288  ptpjopn  17322  dfac14  17328  ptcnplem  17331  txcn  17336  txindis  17344  txdis1cn  17345  ptrescn  17349  txcmplem1  17351  txcmp  17353  txhaus  17357  txlm  17358  tx1stc  17360  txkgen  17362  xkococn  17370  qtopcn  17421  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  hmeoimaf1o  17477  reghmph  17500  nrmhmph  17501  txhmeo  17510  ptuncnv  17514  filcon  17594  fbasrn  17595  fmfnfmlem2  17666  flimfnfcls  17739  cnpfcfi  17751  alexsublem  17754  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  alexsubALT  17761  ptcmplem3  17764  tsmsxp  17853  imasdsf1olem  17953  bl2in  17973  blss  17988  blssex  17989  blcld  18067  stdbdxmet  18077  met1stc  18083  prdsxmslem2  18091  metcnp3  18102  metcnpi3  18108  txmetcnp  18109  nmo0  18260  nmoid  18267  icccmplem1  18343  icccmp  18346  xrge0tsms  18355  metdseq0  18374  cnheiborlem  18468  cnheibor  18469  cnllycmp  18470  pcoval2  18530  cmetcaulem  18730  iscmet3lem1  18733  iscmet3lem2  18734  equivcau  18742  lmcau  18754  cncmet  18760  ivthlem2  18828  ivthlem3  18829  ovoliunlem2  18878  ovolscalem2  18889  uniioombl  18960  dyaddisj  18967  opnmbllem  18972  volivth  18978  ismbfd  19011  ismbf3d  19025  mbfimaopnlem  19026  mbfinf  19036  itg1addlem4  19070  mbfi1fseqlem1  19086  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  itg2seq  19113  itg2lea  19115  itg2split  19120  itg2cnlem1  19132  limciun  19260  dvmptfsum  19338  rolle  19353  c1lip1  19360  dvcnvrelem1  19380  dvcnvre  19382  dvcvx  19383  itgsubst  19412  pf1ind  19454  tdeglem4  19462  mdegmullem  19480  plyco0  19590  coemullem  19647  dgreq0  19662  dgrmul  19667  dgrco  19672  elqaalem2  19716  aannenlem1  19724  aaliou3lem9  19746  ulmres  19783  ulmshftlem  19784  angneg  20117  dcubic  20158  cxploglim  20288  cxploglim2  20289  scvxcvx  20296  basellem3  20336  basellem4  20337  sqff1o  20436  dvdsflip  20438  fsumdvdsdiaglem  20439  dvdsflsumcom  20444  dvdsmulf1o  20450  fsumvma2  20469  logfac2  20472  logfacrlim  20479  logexprlim  20480  dchrelbasd  20494  lgsne0  20588  lgsqrlem2  20597  lgseisenlem2  20605  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  lgsquad2lem2  20614  2sqlem8  20627  2sqlem11  20630  chpo1ubb  20646  vmadivsum  20647  rplogsumlem2  20650  rpvmasumlem  20652  dchrmusum2  20659  dchrvmasumlem1  20660  dchrisum0fno1  20676  dchrisum0re  20678  dchrisum0lem1  20681  dchrisum0lem2  20683  dchrisum0lem3  20684  dchrisum0  20685  mulogsumlem  20696  mulog2sumlem2  20700  vmalogdivsum2  20703  logsqvma  20707  log2sumbnd  20709  selberglem3  20712  selberg  20713  selberg2lem  20715  selberg2b  20717  selberg3lem2  20723  pntrmax  20729  pntrsumo1  20730  pntlemn  20765  pntlemp  20775  qabvle  20790  ostthlem1  20792  ostthlem2  20793  ostth2lem2  20799  ostth3  20803  grpoidinvlem1  20887  grpoidinvlem3  20889  grporcan  20904  ismndo1  21027  isdivrngo  21114  vcsubdir  21128  nmlnoubi  21390  blocnilem  21398  ipblnfi  21450  htthlem  21513  ocsh  21878  shmodsi  21984  pjhthlem2  21987  5oalem2  22250  eigposi  22432  nmopub2tALT  22505  nmfnleub2  22522  nmcexi  22622  nmopcoi  22691  kbass3  22714  mdslmd1lem1  22921  mdslmd1lem2  22922  chirredlem2  22987  chirredlem4  22989  mdsymlem3  23001  mdsymlem5  23003  sumdmdii  23011  sumdmdlem  23014  sumdmdlem2  23015  ballotlemsf1o  23088  xrge0tsmsd  23397  esumpcvgval  23461  imambfm  23582  orvcgteel  23683  orvclteel  23688  txpcon  23778  conpcon  23781  cnllyscon  23791  rellyscon  23797  cvmsss2  23820  cvmlift2lem9  23857  umgra1  23893  iseupa  23896  eupai  23898  relexpsucr  24041  relexpindlem  24051  divelunit  24095  dfon2lem6  24215  trpredmintr  24305  sltres  24389  brbtwn2  24605  colinearalglem4  24609  colinearalg  24610  ax5seglem9  24637  axpaschlem  24640  axcontlem2  24665  axcontlem7  24670  axcontlem8  24671  ifscgr  24739  cgrxfr  24750  btwnconn1lem5  24786  btwnconn1lem6  24787  btwnconn1lem12  24793  brsegle  24803  itg2addnclem  25003  itg2addnc  25005  bddiblnc  25021  mapmapmap  25251  cbicp  25269  oriso  25317  toplat  25393  grpodlcan  25479  trooo  25497  rltrooo  25518  glmrngo  25585  qusp  25645  usptop  25653  limptlimpr2lem1  25677  limptlimpr2lem2  25678  islimrs4  25685  iintlem1  25713  trnij  25718  negveudr  25772  domcmpd  25849  cmpida  25877  cmpmon  25918  clscnc  26113  isib2g1a1  26219  isibg1a2  26220  isibg1a3a  26225  isibg1spa  26226  isibg1a5a  26227  sgplpte21  26235  sgplpte22  26241  finminlem  26334  gtinf  26337  nn0prpwlem  26341  fnessref  26396  refssfne  26397  neibastop1  26411  topjoin  26417  fnemeet2  26419  unirep  26452  frinfm  26519  sdclem2  26555  geomcau  26578  istotbnd3  26598  sstotbnd2  26601  sstotbnd  26602  sstotbnd3  26603  totbndbnd  26616  cntotbnd  26623  ismtyres  26635  heibor1lem  26636  heiborlem1  26638  heiborlem8  26645  unichnidl  26759  ralxpmap  26864  elrfi  26872  nacsfix  26890  fzsplit1nn0  26936  eldioph2  26944  lzenom  26952  irrapxlem3  27012  pellexlem5  27021  pell1234qrne0  27041  pell1234qrmulcl  27043  pell14qrdich  27057  pell1qrge1  27058  pellqrex  27067  reglogltb  27079  reglogleb  27080  rmxypairf1o  27099  rmxycomplete  27105  monotoddzzfi  27130  congadd  27156  congsym  27158  acongrep  27170  jm2.19lem3  27187  jm2.19lem4  27188  jm2.22  27191  jm2.25  27195  expdiophlem1  27217  wepwsolem  27241  kelac1  27264  lmhmfgsplit  27287  pwslnm  27299  frlmlbs  27352  frlmup1  27353  enfixsn  27360  lindfind  27389  islindf3  27399  lindfmm  27400  hbtlem6  27436  hbt  27437  symgsssg  27511  symgfisg  27512  psgnunilem2  27521  psgnghm  27540  mamulid  27561  hashgcdlem  27619  hashgcdeq  27620  mon1psubm  27628  deg1mhm  27629  mulltgt0  27796  fnchoice  27803  climinf  27835  stoweidlem14  27866  stoweidlem17  27869  stoweidlem34  27886  f1oprg  28186  uslgra1  28252  usgra1  28253  nb3graprlem1  28287  nbcusgra  28298  uvtxnbgravtx  28308  wlkntrllem5  28349  bnj1110  29328  bnj1118  29330  cvlcvr1  30151  ishlat3N  30166  llnmlplnN  30350  islvol2aN  30403  4atlem4c  30412  4atlem4d  30413  isline2  30585  isline3  30587  linepsubclN  30762  lhpexle3lem  30822  lhpjat2  30832  cdlemd4  31012  cdleme0cq  31026  cdleme32fva  31248  cdleme32fvaw  31250  tendo0mul  31637  tendo0mulr  31638  diameetN  31868  dvhvaddcl  31907  dvhvaddcomN  31908  cdlemm10N  31930  dvadiaN  31940  djavalN  31947  dihvalcqat  32051  dihopelvalcpre  32060  djhval  32210  dihjat1lem  32240
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 177  df-an 360
  Copyright terms: Public domain W3C validator