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

Theorem ad2antrl 709
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 452 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantl 453 1  |-  ( ( ch  /\  ( ph  /\ 
th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simprl  733  simprll  739  simprlr  740  fr2nr  4520  tz7.7  4567  reusv2lem4  4686  onint  4734  ordsucelsuc  4761  somin1  5229  elxp5  5317  f1oprg  5677  soisores  6006  wemoiso  6037  wemoiso2  6038  sorpssi  6487  tz7.48lem  6657  oalimcl  6762  oeeui  6804  oaabs2  6847  omabs  6849  swoer  6892  0er  6899  pw2f1olem  7171  mapxpen  7232  mapunen  7235  unxpdomlem2  7273  unxpdomlem3  7274  findcard3  7309  isfinite2  7324  domunfican  7338  fodomfi  7344  fissuni  7369  fipreima  7370  indexfi  7372  marypha1lem  7396  marypha2  7402  supmo  7413  oieu  7464  brwdom2  7497  ixpiunwdom  7515  cantnfval2  7580  cantnfle  7582  cantnflt  7583  cantnf  7605  wemapwe  7610  cnfcom  7613  rankonidlem  7710  r1pwcl  7729  infxpenlem  7851  infxpenc2lem1  7856  fseqenlem1  7861  dfac8clem  7869  mappwen  7949  dfac3  7958  dfac5  7965  dfac12lem3  7981  cdainf  8028  infunsdom  8050  coftr  8109  ssfin4  8146  domfin4  8147  fin23lem26  8161  fin23lem22  8163  fin23lem28  8176  fin23lem32  8180  fin23lem40  8187  isf32lem5  8193  compssiso  8210  isf34lem4  8213  isfin1-3  8222  fin1a2lem13  8248  hsmexlem2  8263  hsmexlem4  8265  zorn2lem1  8332  ttukeylem6  8350  iundom2g  8371  konigthlem  8399  pwcfsdom  8414  fpwwe2lem12  8472  fpwwe2  8474  pwfseqlem3  8491  winalim2  8527  r1wunlim  8568  inttsk  8605  inar1  8606  grur1  8651  nqereq  8768  ltexprlem7  8875  prlem936  8880  00id  9197  addid2  9205  ltord1  9509  divdiv1  9681  divdiv2  9682  conjmul  9687  ltdivmul  9838  ledivmul  9839  lt2mul2div  9842  ltdiv23  9857  lediv23  9858  lediv12a  9859  ledivp1  9868  peano2uz2  10313  peano5uzi  10314  eluzp1m1  10465  qbtwnre  10741  xralrple  10747  xleadd1a  10788  xmulge0  10819  xmulass  10822  xlemul1a  10823  iooshf  10945  modadd1  11233  modmul1  11234  seqcl2  11296  seqfveq2  11300  seqid2  11324  seqhomo  11325  seqdistr  11329  mulexpz  11375  leexp2r  11392  expnlbnd2  11465  expmulnbnd  11466  hashmap  11653  hashfun  11655  hashbclem  11656  hashfacen  11658  hashf1lem2  11660  hashf1  11661  splid  11737  wrdind  11746  sqrlem1  12003  sqrlem6  12008  rlim  12244  rlimclim1  12294  climsup  12418  caurcvg2  12426  caucvgb  12428  iseralt  12433  sumss  12473  fsum2dlem  12509  fsumshft  12518  o1fsum  12547  incexclem  12571  divrcnv  12587  flo1  12589  ruclem6  12789  moddvds  12814  dvdseq  12852  bitsf1ocnv  12911  bitsf1  12913  sadcaddlem  12924  bezoutlem2  12994  bezoutlem4  12996  prmind2  13045  isprm6  13064  isprm5  13067  hashdvds  13119  crt  13122  eulerthlem2  13126  prmdiveq  13130  iserodd  13164  pclem  13167  pcprendvds2  13170  pcexp  13188  pcneg  13202  pc2dvds  13207  pcmpt  13216  prmpwdvds  13227  pockthg  13229  prmreclem5  13243  4sqlem11  13278  ramub2  13337  ramubcl  13341  ram0  13345  ramub1lem2  13350  ramcl  13352  setscom  13452  sscpwex  13970  setcinv  14200  1stfcl  14249  2ndfcl  14250  hofpropd  14319  isacs3lem  14547  isacs4lem  14549  acsmap2d  14560  submnd0  14680  subsubm  14712  frmdup1  14764  frmdup3  14766  isgrpinv  14810  subsubg  14918  cycsubgcl  14921  conjghm  14991  divsghm  14997  gsumwrev  15117  odf1o2  15162  sylow1lem1  15187  odcau  15193  pgpfi  15194  pgpssslw  15203  fislw  15214  efgtlen  15313  efginvrel2  15314  efgrelexlemb  15337  efgredeu  15339  efgcpbllemb  15342  frgpup1  15362  cygabl  15455  lt6abl  15459  gsum2d  15501  gsum2d2lem  15502  gsum2d2  15503  dmdprdsplit2lem  15558  ablfacrp  15579  pgpfac1lem3  15590  irredrmul  15767  subsubrg  15849  islss4  15993  lspextmo  16087  lspsnat  16172  issubassa  16338  resspsradd  16434  resspsrmul  16435  coe1tmmul2  16623  prmirredlem  16728  znf1o  16787  znidomb  16797  frgpcyg  16809  tgcl  16989  pptbas  17027  clsval2  17069  mretopd  17111  lmbr2  17277  cncls2  17291  nrmsep  17375  regsep2  17394  cmpsublem  17416  cmpsub  17417  tgcmp  17418  uncmp  17420  hauscmplem  17423  iunconlem  17443  1stcrest  17469  2ndcctbss  17471  2ndcsep  17475  dis2ndc  17476  hausllycmp  17510  dislly  17513  kgentopon  17523  1stckgen  17539  kgencn3  17543  ptpjpre1  17556  ptbasin  17562  ptpjopn  17597  dfac14  17603  ptcnplem  17606  txcn  17611  txindis  17619  txdis1cn  17620  ptrescn  17624  txcmplem1  17626  txcmp  17628  txhaus  17632  txlm  17633  tx1stc  17635  txkgen  17637  xkococn  17645  qtopcn  17699  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  hmeoimaf1o  17755  reghmph  17778  nrmhmph  17779  txhmeo  17788  ptuncnv  17792  filcon  17868  fbasrn  17869  fmfnfmlem2  17940  flimfnfcls  18013  cnpfcfi  18025  alexsublem  18028  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem3  18038  cnextfval  18046  tsmsxp  18137  imasdsf1olem  18356  bl2in  18383  blssps  18407  blss  18408  blssexps  18409  blssex  18410  blcld  18488  stdbdxmet  18498  met1stc  18504  prdsxmslem2  18512  metcnp3  18523  metcnpi3  18529  txmetcnp  18530  nmo0  18722  nmoid  18729  icccmplem1  18806  icccmp  18809  xrge0tsms  18818  metdseq0  18837  cnheiborlem  18932  cnheibor  18933  cnllycmp  18934  pcoval2  18994  cmetcaulem  19194  iscmet3lem1  19197  iscmet3lem2  19198  equivcau  19206  lmcau  19218  cncmet  19228  ivthlem2  19302  ivthlem3  19303  ovoliunlem2  19352  ovolscalem2  19363  uniioombl  19434  dyaddisj  19441  opnmbllem  19446  volivth  19452  ismbfd  19485  ismbf3d  19499  mbfimaopnlem  19500  mbfinf  19510  itg1addlem4  19544  mbfi1fseqlem1  19560  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  itg2seq  19587  itg2lea  19589  itg2split  19594  itg2cnlem1  19606  limciun  19734  dvmptfsum  19812  rolle  19827  c1lip1  19834  dvcnvrelem1  19854  dvcnvre  19856  dvcvx  19857  itgsubst  19886  pf1ind  19928  tdeglem4  19936  mdegmullem  19954  plyco0  20064  coemullem  20121  dgreq0  20136  dgrmul  20141  dgrco  20146  elqaalem2  20190  aannenlem1  20198  aaliou3lem9  20220  ulmres  20257  ulmshftlem  20258  angneg  20598  dcubic  20639  cxploglim  20769  cxploglim2  20770  scvxcvx  20777  basellem3  20818  basellem4  20819  sqff1o  20918  dvdsflip  20920  fsumdvdsdiaglem  20921  dvdsflsumcom  20926  dvdsmulf1o  20932  fsumvma2  20951  logfac2  20954  logfacrlim  20961  logexprlim  20962  dchrelbasd  20976  lgsne0  21070  lgsqrlem2  21079  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad2lem2  21096  2sqlem8  21109  2sqlem11  21112  chpo1ubb  21128  vmadivsum  21129  rplogsumlem2  21132  rpvmasumlem  21134  dchrmusum2  21141  dchrvmasumlem1  21142  dchrisum0fno1  21158  dchrisum0re  21160  dchrisum0lem1  21163  dchrisum0lem2  21165  dchrisum0lem3  21166  dchrisum0  21167  mulogsumlem  21178  mulog2sumlem2  21182  vmalogdivsum2  21185  logsqvma  21189  log2sumbnd  21191  selberglem3  21194  selberg  21195  selberg2lem  21197  selberg2b  21199  selberg3lem2  21205  pntrmax  21211  pntrsumo1  21212  pntlemn  21247  pntlemp  21257  qabvle  21272  ostthlem1  21274  ostthlem2  21275  ostth2lem2  21281  ostth3  21285  umgra1  21314  uslgra1  21345  nb3graprlem1  21413  nbcusgra  21425  uvtxnbgravtx  21457  wlkntrllem3  21514  vdgrf  21622  iseupa  21640  eupai  21642  grpoidinvlem1  21745  grpoidinvlem3  21747  grporcan  21762  ismndo1  21885  isdivrngo  21972  vcsubdir  21988  nmlnoubi  22250  blocnilem  22258  ipblnfi  22310  htthlem  22373  ocsh  22738  shmodsi  22844  pjhthlem2  22847  5oalem2  23110  eigposi  23292  nmopub2tALT  23365  nmfnleub2  23382  nmcexi  23482  nmopcoi  23551  kbass3  23574  mdslmd1lem1  23781  mdslmd1lem2  23782  chirredlem2  23847  chirredlem4  23849  mdsymlem3  23861  mdsymlem5  23863  sumdmdii  23871  sumdmdlem  23874  sumdmdlem2  23875  disjxpin  23981  xrge0tsmsd  24176  pstmxmet  24245  qqhghm  24325  qqhrhm  24326  esumpcvgval  24421  volmeas  24540  imambfm  24565  dya2iocnrect  24584  orvcgteel  24678  orvclteel  24683  ballotlemsf1o  24724  lgamgulmlem5  24770  lgamcvg2  24792  txpcon  24872  conpcon  24875  cnllyscon  24885  rellyscon  24891  cvmsss2  24914  cvmlift2lem9  24951  relexpsucr  25083  relexpindlem  25092  divelunit  25138  fprodshft  25253  fprodrev  25254  fprod2dlem  25257  dfon2lem6  25358  trpredmintr  25448  sltres  25532  brbtwn2  25748  colinearalglem4  25752  colinearalg  25753  ax5seglem9  25780  axpaschlem  25783  axcontlem2  25808  axcontlem7  25813  axcontlem8  25814  ifscgr  25882  cgrxfr  25893  btwnconn1lem5  25929  btwnconn1lem6  25930  btwnconn1lem12  25936  brsegle  25946  mblfinlem  26143  mblfinlem3  26145  ismblfin  26146  mbfresfi  26152  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  bddiblnc  26174  finminlem  26211  gtinf  26212  nn0prpwlem  26215  fnessref  26263  refssfne  26264  neibastop1  26278  topjoin  26284  fnemeet2  26286  unirep  26304  frinfm  26327  sdclem2  26336  geomcau  26355  istotbnd3  26370  sstotbnd2  26373  sstotbnd  26374  sstotbnd3  26375  totbndbnd  26388  cntotbnd  26395  ismtyres  26407  heibor1lem  26408  heiborlem1  26410  heiborlem8  26417  unichnidl  26531  ralxpmap  26632  elrfi  26638  nacsfix  26656  fzsplit1nn0  26702  eldioph2  26710  lzenom  26718  irrapxlem3  26777  pellexlem5  26786  pell1234qrne0  26806  pell1234qrmulcl  26808  pell14qrdich  26822  pell1qrge1  26823  pellqrex  26832  reglogltb  26844  reglogleb  26845  rmxypairf1o  26864  rmxycomplete  26870  monotoddzzfi  26895  congadd  26921  congsym  26923  acongrep  26935  jm2.19lem3  26952  jm2.19lem4  26953  jm2.22  26956  jm2.25  26960  expdiophlem1  26982  wepwsolem  27006  kelac1  27029  lmhmfgsplit  27052  pwslnm  27064  frlmlbs  27117  frlmup1  27118  enfixsn  27125  lindfind  27154  islindf3  27164  lindfmm  27165  hbtlem6  27201  hbt  27202  symgsssg  27276  symgfisg  27277  psgnunilem2  27286  psgnghm  27305  mamulid  27326  hashgcdlem  27384  hashgcdeq  27385  mon1psubm  27393  deg1mhm  27394  mulltgt0  27560  fnchoice  27567  climinf  27599  stoweidlem14  27630  stoweidlem17  27633  stoweidlem34  27650  stoweidlem50  27666  el2xptp0  27949  swrdswrd  28011  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12lem1  28019  swrdccatin12  28026  swrdccat3b  28031  n4cyclfrgra  28122  frgrawopreg  28152  2spotdisj  28164  bnj1110  29057  bnj1118  29059  cvlcvr1  29822  ishlat3N  29837  llnmlplnN  30021  islvol2aN  30074  4atlem4c  30083  4atlem4d  30084  isline2  30256  isline3  30258  linepsubclN  30433  lhpexle3lem  30493  lhpjat2  30503  cdlemd4  30683  cdleme0cq  30697  cdleme32fva  30919  cdleme32fvaw  30921  tendo0mul  31308  tendo0mulr  31309  diameetN  31539  dvhvaddcl  31578  dvhvaddcomN  31579  cdlemm10N  31601  dvadiaN  31611  djavalN  31618  dihvalcqat  31722  dihopelvalcpre  31731  djhval  31881  dihjat1lem  31911
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 178  df-an 361
  Copyright terms: Public domain W3C validator