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

Theorem ad2antrl 710
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 453 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantl 454 1  |-  ( ( ch  /\  ( ph  /\ 
th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  simprl  734  simprll  740  simprlr  741  sbcom  2166  fr2nr  4562  tz7.7  4609  reusv2lem4  4729  onint  4777  ordsucelsuc  4804  somin1  5272  elxp5  5360  f1oprg  5720  soisores  6049  wemoiso  6080  wemoiso2  6081  sorpssi  6530  tz7.48lem  6700  oalimcl  6805  oeeui  6847  oaabs2  6890  omabs  6892  swoer  6935  0er  6942  pw2f1olem  7214  mapxpen  7275  mapunen  7278  unxpdomlem2  7316  unxpdomlem3  7317  findcard3  7352  isfinite2  7367  domunfican  7381  fodomfi  7387  fissuni  7413  fipreima  7414  indexfi  7416  marypha1lem  7440  marypha2  7446  supmo  7459  oieu  7510  brwdom2  7543  ixpiunwdom  7561  cantnfval2  7626  cantnfle  7628  cantnflt  7629  cantnf  7651  wemapwe  7656  cnfcom  7659  rankonidlem  7756  r1pwcl  7775  infxpenlem  7897  infxpenc2lem1  7902  fseqenlem1  7907  dfac8clem  7915  mappwen  7995  dfac3  8004  dfac5  8011  dfac12lem3  8027  cdainf  8074  infunsdom  8096  coftr  8155  ssfin4  8192  domfin4  8193  fin23lem26  8207  fin23lem22  8209  fin23lem28  8222  fin23lem32  8226  fin23lem40  8233  isf32lem5  8239  compssiso  8256  isf34lem4  8259  isfin1-3  8268  fin1a2lem13  8294  hsmexlem2  8309  hsmexlem4  8311  zorn2lem1  8378  ttukeylem6  8396  iundom2g  8417  konigthlem  8445  pwcfsdom  8460  fpwwe2lem12  8518  fpwwe2  8520  pwfseqlem3  8537  winalim2  8573  r1wunlim  8614  inttsk  8651  inar1  8652  grur1  8697  nqereq  8814  ltexprlem7  8921  prlem936  8926  00id  9243  addid2  9251  ltord1  9555  divdiv1  9727  divdiv2  9728  conjmul  9733  ltdivmul  9884  ledivmul  9885  lt2mul2div  9888  ltdiv23  9903  lediv23  9904  lediv12a  9905  ledivp1  9914  peano2uz2  10359  peano5uzi  10360  eluzp1m1  10511  qbtwnre  10787  xralrple  10793  xleadd1a  10834  xmulge0  10865  xmulass  10868  xlemul1a  10869  iooshf  10991  modadd1  11280  modmul1  11281  seqcl2  11343  seqfveq2  11347  seqid2  11371  seqhomo  11372  seqdistr  11376  mulexpz  11422  leexp2r  11439  expnlbnd2  11512  expmulnbnd  11513  hashmap  11700  hashfun  11702  hashbclem  11703  hashfacen  11705  hashf1lem2  11707  hashf1  11708  splid  11784  wrdind  11793  sqrlem1  12050  sqrlem6  12055  rlim  12291  rlimclim1  12341  climsup  12465  caurcvg2  12473  caucvgb  12475  iseralt  12480  sumss  12520  fsum2dlem  12556  fsumshft  12565  o1fsum  12594  incexclem  12618  divrcnv  12634  flo1  12636  ruclem6  12836  moddvds  12861  dvdseq  12899  bitsf1ocnv  12958  bitsf1  12960  sadcaddlem  12971  bezoutlem2  13041  bezoutlem4  13043  prmind2  13092  isprm6  13111  isprm5  13114  hashdvds  13166  crt  13169  eulerthlem2  13173  prmdiveq  13177  iserodd  13211  pclem  13214  pcprendvds2  13217  pcexp  13235  pcneg  13249  pc2dvds  13254  pcmpt  13263  prmpwdvds  13274  pockthg  13276  prmreclem5  13290  4sqlem11  13325  ramub2  13384  ramubcl  13388  ram0  13392  ramub1lem2  13397  ramcl  13399  setscom  13499  sscpwex  14017  setcinv  14247  1stfcl  14296  2ndfcl  14297  hofpropd  14366  isacs3lem  14594  isacs4lem  14596  acsmap2d  14607  submnd0  14727  subsubm  14759  frmdup1  14811  frmdup3  14813  isgrpinv  14857  subsubg  14965  cycsubgcl  14968  conjghm  15038  divsghm  15044  gsumwrev  15164  odf1o2  15209  sylow1lem1  15234  odcau  15240  pgpfi  15241  pgpssslw  15250  fislw  15261  efgtlen  15360  efginvrel2  15361  efgrelexlemb  15384  efgredeu  15386  efgcpbllemb  15389  frgpup1  15409  cygabl  15502  lt6abl  15506  gsum2d  15548  gsum2d2lem  15549  gsum2d2  15550  dmdprdsplit2lem  15605  ablfacrp  15626  pgpfac1lem3  15637  irredrmul  15814  subsubrg  15896  islss4  16040  lspextmo  16134  lspsnat  16219  issubassa  16385  resspsradd  16481  resspsrmul  16482  coe1tmmul2  16670  prmirredlem  16775  znf1o  16834  znidomb  16844  frgpcyg  16856  tgcl  17036  pptbas  17074  clsval2  17116  mretopd  17158  lmbr2  17325  cncls2  17339  nrmsep  17423  regsep2  17442  cmpsublem  17464  cmpsub  17465  tgcmp  17466  uncmp  17468  hauscmplem  17471  iunconlem  17492  1stcrest  17518  2ndcctbss  17520  2ndcsep  17524  dis2ndc  17525  hausllycmp  17559  dislly  17562  kgentopon  17572  1stckgen  17588  kgencn3  17592  ptpjpre1  17605  ptbasin  17611  ptpjopn  17646  dfac14  17652  ptcnplem  17655  txcn  17660  txindis  17668  txdis1cn  17669  ptrescn  17673  txcmplem1  17675  txcmp  17677  txhaus  17681  txlm  17682  tx1stc  17684  txkgen  17686  xkococn  17694  qtopcn  17748  kqreglem1  17775  kqreglem2  17776  kqnrmlem1  17777  kqnrmlem2  17778  hmeoimaf1o  17804  reghmph  17827  nrmhmph  17828  txhmeo  17837  ptuncnv  17841  filcon  17917  fbasrn  17918  fmfnfmlem2  17989  flimfnfcls  18062  cnpfcfi  18074  alexsublem  18077  alexsubALTlem2  18081  alexsubALTlem3  18082  alexsubALTlem4  18083  alexsubALT  18084  ptcmplem3  18087  cnextfval  18095  tsmsxp  18186  imasdsf1olem  18405  bl2in  18432  blssps  18456  blss  18457  blssexps  18458  blssex  18459  blcld  18537  stdbdxmet  18547  met1stc  18553  prdsxmslem2  18561  metcnp3  18572  metcnpi3  18578  txmetcnp  18579  nmo0  18771  nmoid  18778  icccmplem1  18855  icccmp  18858  xrge0tsms  18867  metdseq0  18886  cnheiborlem  18981  cnheibor  18982  cnllycmp  18983  pcoval2  19043  cmetcaulem  19243  iscmet3lem1  19246  iscmet3lem2  19247  equivcau  19255  lmcau  19267  cncmet  19277  ivthlem2  19351  ivthlem3  19352  ovoliunlem2  19401  ovolscalem2  19412  uniioombl  19483  dyaddisj  19490  opnmbllem  19495  volivth  19501  ismbfd  19534  ismbf3d  19548  mbfimaopnlem  19549  mbfinf  19559  itg1addlem4  19593  mbfi1fseqlem1  19609  mbfi1fseqlem3  19611  mbfi1fseqlem4  19612  mbfi1fseqlem5  19613  mbfi1fseqlem6  19614  itg2seq  19636  itg2lea  19638  itg2split  19643  itg2cnlem1  19655  limciun  19783  dvmptfsum  19861  rolle  19876  c1lip1  19883  dvcnvrelem1  19903  dvcnvre  19905  dvcvx  19906  itgsubst  19935  pf1ind  19977  tdeglem4  19985  mdegmullem  20003  plyco0  20113  coemullem  20170  dgreq0  20185  dgrmul  20190  dgrco  20195  elqaalem2  20239  aannenlem1  20247  aaliou3lem9  20269  ulmres  20306  ulmshftlem  20307  angneg  20647  dcubic  20688  cxploglim  20818  cxploglim2  20819  scvxcvx  20826  basellem3  20867  basellem4  20868  sqff1o  20967  dvdsflip  20969  fsumdvdsdiaglem  20970  dvdsflsumcom  20975  dvdsmulf1o  20981  fsumvma2  21000  logfac2  21003  logfacrlim  21010  logexprlim  21011  dchrelbasd  21025  lgsne0  21119  lgsqrlem2  21128  lgseisenlem2  21136  lgsquadlem1  21140  lgsquadlem2  21141  lgsquadlem3  21142  lgsquad2lem2  21145  2sqlem8  21158  2sqlem11  21161  chpo1ubb  21177  vmadivsum  21178  rplogsumlem2  21181  rpvmasumlem  21183  dchrmusum2  21190  dchrvmasumlem1  21191  dchrisum0fno1  21207  dchrisum0re  21209  dchrisum0lem1  21212  dchrisum0lem2  21214  dchrisum0lem3  21215  dchrisum0  21216  mulogsumlem  21227  mulog2sumlem2  21231  vmalogdivsum2  21234  logsqvma  21238  log2sumbnd  21240  selberglem3  21243  selberg  21244  selberg2lem  21246  selberg2b  21248  selberg3lem2  21254  pntrmax  21260  pntrsumo1  21261  pntlemn  21296  pntlemp  21306  qabvle  21321  ostthlem1  21323  ostthlem2  21324  ostth2lem2  21330  ostth3  21334  umgra1  21363  uslgra1  21394  nb3graprlem1  21462  nbcusgra  21474  uvtxnbgravtx  21506  wlkntrllem3  21563  vdgrf  21671  iseupa  21689  eupai  21691  grpoidinvlem1  21794  grpoidinvlem3  21796  grporcan  21811  ismndo1  21934  isdivrngo  22021  vcsubdir  22037  nmlnoubi  22299  blocnilem  22307  ipblnfi  22359  htthlem  22422  ocsh  22787  shmodsi  22893  pjhthlem2  22896  5oalem2  23159  eigposi  23341  nmopub2tALT  23414  nmfnleub2  23431  nmcexi  23531  nmopcoi  23600  kbass3  23623  mdslmd1lem1  23830  mdslmd1lem2  23831  chirredlem2  23896  chirredlem4  23898  mdsymlem3  23910  mdsymlem5  23912  sumdmdii  23920  sumdmdlem  23923  sumdmdlem2  23924  disjxpin  24030  xrge0tsmsd  24225  pstmxmet  24294  qqhghm  24374  qqhrhm  24375  esumpcvgval  24470  volmeas  24589  imambfm  24614  dya2iocnrect  24633  orvcgteel  24727  orvclteel  24732  ballotlemsf1o  24773  lgamgulmlem5  24819  lgamcvg2  24841  txpcon  24921  conpcon  24924  cnllyscon  24934  rellyscon  24940  cvmsss2  24963  cvmlift2lem9  25000  relexpsucr  25132  relexpindlem  25141  divelunit  25187  fprodshft  25302  fprodrev  25303  fprod2dlem  25306  dfon2lem6  25417  trpredmintr  25511  wzel  25577  sltres  25621  brbtwn2  25846  colinearalglem4  25850  colinearalg  25851  ax5seglem9  25878  axpaschlem  25881  axcontlem2  25906  axcontlem7  25911  axcontlem8  25912  ifscgr  25980  cgrxfr  25991  btwnconn1lem5  26027  btwnconn1lem6  26028  btwnconn1lem12  26034  brsegle  26044  opnmbllem0  26244  mblfinlem1  26245  mblfinlem4  26248  ismblfin  26249  mbfresfi  26255  itg2addnclem  26258  itg2addnclem3  26260  itg2addnc  26261  bddiblnc  26277  finminlem  26323  gtinf  26324  nn0prpwlem  26327  fnessref  26375  refssfne  26376  neibastop1  26390  topjoin  26396  fnemeet2  26398  unirep  26416  frinfm  26439  sdclem2  26448  geomcau  26467  istotbnd3  26482  sstotbnd2  26485  sstotbnd  26486  sstotbnd3  26487  totbndbnd  26500  cntotbnd  26507  ismtyres  26519  heibor1lem  26520  heiborlem1  26522  heiborlem8  26529  unichnidl  26643  ralxpmap  26744  elrfi  26750  nacsfix  26768  fzsplit1nn0  26814  eldioph2  26822  lzenom  26830  irrapxlem3  26889  pellexlem5  26898  pell1234qrne0  26918  pell1234qrmulcl  26920  pell14qrdich  26934  pell1qrge1  26935  pellqrex  26944  reglogltb  26956  reglogleb  26957  rmxypairf1o  26976  rmxycomplete  26982  monotoddzzfi  27007  congadd  27033  congsym  27035  acongrep  27047  jm2.19lem3  27064  jm2.19lem4  27065  jm2.22  27068  jm2.25  27072  expdiophlem1  27094  wepwsolem  27118  kelac1  27140  lmhmfgsplit  27163  pwslnm  27175  frlmlbs  27228  frlmup1  27229  enfixsn  27236  lindfind  27265  islindf3  27275  lindfmm  27276  hbtlem6  27312  hbt  27313  symgsssg  27387  symgfisg  27388  psgnunilem2  27397  psgnghm  27416  mamulid  27437  hashgcdlem  27495  hashgcdeq  27496  mon1psubm  27504  deg1mhm  27505  mulltgt0  27671  fnchoice  27678  climinf  27710  stoweidlem14  27741  stoweidlem17  27744  stoweidlem34  27761  stoweidlem50  27777  el2xptp0  28064  elovmpt2rab1  28093  nn0nndivcl  28152  nn0ge0div  28153  ccatsymb  28199  swrdswrd  28221  swrdccatin1  28227  swrdccatin2  28232  swrdccatin12  28236  swrdccat  28238  2cshwmod  28279  cshweqrep  28296  n4cyclfrgra  28470  frgrawopreg  28500  2spotdisj  28512  bnj1110  29413  bnj1118  29415  cvlcvr1  30199  ishlat3N  30214  llnmlplnN  30398  islvol2aN  30451  4atlem4c  30460  4atlem4d  30461  isline2  30633  isline3  30635  linepsubclN  30810  lhpexle3lem  30870  lhpjat2  30880  cdlemd4  31060  cdleme0cq  31074  cdleme32fva  31296  cdleme32fvaw  31298  tendo0mul  31685  tendo0mulr  31686  diameetN  31916  dvhvaddcl  31955  dvhvaddcomN  31956  cdlemm10N  31978  dvadiaN  31988  djavalN  31995  dihvalcqat  32099  dihopelvalcpre  32108  djhval  32258  dihjat1lem  32288
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