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

Theorem ad2antll 761
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad2antll ((𝜒 ∧ (𝜃𝜑)) → 𝜓)

Proof of Theorem ad2antll
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantl 481 . 2 ((𝜃𝜑) → 𝜓)
32adantl 481 1 ((𝜒 ∧ (𝜃𝜑)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  simprr  792  simprrl  800  simprrr  801  prneimg  4328  fr2nr  5016  wereu2  5035  f1oprg  6093  fvtp1g  6368  funfvima3  6399  isof1oidb  6474  isomin  6487  weniso  6504  elovmpt3rab1  6791  sorpssi  6841  tfrlem9a  7369  oalimcl  7527  odi  7546  oeeui  7569  ralxpmap  7793  boxriin  7836  domdifsn  7928  domunsncan  7945  enfixsn  7954  disjen  8002  mapen  8009  mapxpen  8011  mapunen  8014  unxpdomlem2  8050  unxpdomlem3  8051  findcard2d  8087  findcard3  8088  isfinite2  8103  marypha1lem  8222  marypha2  8228  supmo  8241  infmo  8284  card2inf  8343  brwdom2  8361  wemapwe  8477  rankonidlem  8574  rankxplim3  8627  infxpenlem  8719  infxpenc2lem1  8725  infxpenc2  8728  fseqenlem1  8730  fseqenlem2  8731  infpwfien  8768  dfac12lem2  8849  infunsdom1  8918  infunsdom  8919  infmap2  8923  fin2i2  9023  fin23lem28  9045  fin23lem32  9049  fin23lem34  9051  fin23lem40  9056  isf32lem2  9059  compssiso  9079  isfin1-3  9091  fin1a2lem10  9114  fin12  9118  hsmexlem4  9134  ac6num  9184  ttukeylem7  9220  axdclem2  9225  iundom2g  9241  fpwwe2lem12  9342  pwfseqlem3  9361  winalim2  9397  winafp  9398  wunex2  9439  grur1  9521  dedekindle  10080  00id  10090  receu  10551  lt2mul2div  10780  peano5uzi  11342  uzwo  11627  qbtwnre  11904  iooshf  12123  modmul1  12585  seqcl2  12681  seqfveq2  12685  seqid2  12709  seqdistr  12714  expcl2lem  12734  mulexpz  12762  expnlbnd2  12857  hashfun  13084  hashfacen  13095  hashf1lem1  13096  elss2prb  13123  fstwrdne0  13200  swrdswrd  13312  wrd2ind  13329  splid  13355  repswrevw  13384  cshwidx0  13403  2cshw  13410  cshweqrep  13418  cshw1  13419  wwlktovfo  13549  relexpfld  13637  relexpindlem  13651  sqrlem6  13836  absexpz  13893  o1rlimmul  14197  iseralt  14263  summolem2  14294  fsumf1o  14301  fsum0diag2  14357  fsummulc2  14358  cvgcmpce  14391  incexclem  14407  prodmolem2  14504  fprodcl2lem  14519  fprodmul  14529  fprodrev  14546  moddvds  14829  dvdsflip  14877  bitsf1ocnv  15004  sadcaddlem  15017  bezoutlem2  15095  bezoutlem4  15097  dfgcd2  15101  lcmgcdlem  15157  crth  15321  hashgcdlem  15331  phisum  15333  pcqcl  15399  pcid  15415  pcneg  15416  prmpwdvds  15446  pockthg  15448  4sqlem11  15497  ramub2  15556  0ram  15562  prmgaplem7  15599  prmgaplem8  15600  setscom  15731  qusval  16025  initoeu1  16484  termoeu1  16491  setcinv  16563  funcestrcsetclem9  16611  funcsetcestrclem9  16626  fullsetcestrc  16629  1stfcl  16660  2ndfcl  16661  hofpropd  16730  isacs3lem  16989  frmdss2  17223  frmdup1  17224  mgm2nsgrplem2  17229  mulgdirlem  17395  mulgass  17402  cycsubgcl  17443  0nsg  17462  ghmmulg  17495  conjghm  17514  qusghm  17520  gsumwrev  17619  symg2bas  17641  symgfixelsi  17678  f1otrspeq  17690  psgnunilem2  17738  psgnunilem3  17739  odf1o2  17811  lsmhash  17941  efgtf  17958  efgredeu  17988  efgcpbllemb  17991  frgpuplem  18008  frgpup1  18011  cygabl  18115  ghmcyg  18120  gsumval3lem1  18129  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumconst  18157  gsumzmhm  18160  gsumzoppg  18167  gsum2d  18194  subgdmdprd  18256  pgpfac1lem3  18299  gsummgp0  18431  islmodd  18692  islss3  18780  0lmhm  18861  idlmhm  18862  lmhmeql  18876  pwssplit3  18882  lidldvgen  19076  evlslem1  19336  coe1tmmul2  19467  pf1ind  19540  qsssubdrg  19624  cnsubrg  19625  znf1o  19719  psgnghm  19745  psgndif  19767  cssmre  19856  dsmmsubg  19906  frlmup1  19956  lindfrn  19979  f1lindf  19980  mamufval  20010  mamurid  20067  mvmulfval  20167  mdetralt2  20234  mndifsplit  20261  maducoeval2  20265  madugsum  20268  mat2pmatmul  20355  decpmatmul  20396  pm2mpf1lem  20418  pm2mpf1  20423  monmat2matmon  20448  chpscmat  20466  fvmptnn04if  20473  tgcl  20584  ppttop  20621  epttop  20623  clsval2  20664  opncldf1  20698  mretopd  20706  neindisj  20731  neiptopnei  20746  restcls  20795  restntr  20796  ordtbas  20806  cnpnei  20878  cncls2  20887  tgcmp  21014  cmpcld  21015  uncmp  21016  hauscmplem  21019  1stcfb  21058  2ndcctbss  21068  hauspwdom  21114  reftr  21127  comppfsc  21145  kgentopon  21151  ptpjpre1  21184  ptcnplem  21234  txcn  21239  txdis1cn  21248  txhaus  21260  xkopt  21268  imasnopn  21303  imasncld  21304  imasncls  21305  hmeoimaf1o  21383  cmphaushmeo  21413  txhmeo  21416  trfbas2  21457  fbasfip  21482  fbasrn  21498  fmss  21560  elfm2  21562  hauspwpwf1  21601  flfcnp  21618  fclscf  21639  flimfnfcls  21642  fcfval  21647  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem3  21668  ptcmplem4  21669  cnextfval  21676  cnextcn  21681  tmdgsum2  21710  ustex2sym  21830  neipcfilu  21910  imasdsf1olem  21988  metss2lem  22126  stdbdxmet  22130  stdbdmopn  22133  metrest  22139  metcnp  22156  restmetu  22185  tngngp  22268  icccmplem1  22433  icccvx  22557  evth  22566  lebnumlem1  22568  pi1blem  22647  isncvsngp  22757  equivcau  22906  bcthlem5  22933  ivthlem3  23029  ovolicc2lem3  23094  ovolicc2lem4  23095  dyaddisj  23170  dyadmbllem  23173  ismbfd  23213  itg2seq  23315  itgss  23384  limciun  23464  dvcobr  23515  dvmptfsum  23542  c1liplem1  23563  c1lip1  23564  lhop  23583  dvcvx  23587  plyco0  23752  elply2  23756  plypf1  23772  dgreq0  23825  elqaalem2  23879  aalioulem6  23896  aaliou  23897  aaliou2b  23900  ulmss  23955  ulmcn  23957  pserulm  23980  lgamgulmlem5  24559  basellem4  24610  fsumdvdsdiaglem  24709  dvdsmulf1o  24720  chtublem  24736  fsumvma2  24739  logfaclbnd  24747  dchrelbasd  24764  lgsqrlem2  24872  gausslemma2dlem1a  24890  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  rplogsumlem2  24974  rpvmasumlem  24976  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  rpvmasum2  25001  dchrisum0lem1  25005  logsqvma  25031  selberg4  25050  pntibndlem3  25081  pntlem3  25098  ostthlem1  25116  ostthlem2  25117  idmot  25232  brcgr  25580  brbtwn2  25585  axsegconlem8  25604  axpaschlem  25620  axeuclid  25643  axcontlem2  25645  axcontlem7  25650  eengtrkg  25665  upgrex  25759  umgraex  25852  nbgraf1olem5  25974  nb3graprlem1  25980  usgrasscusgra  26011  wlks  26047  usgra2wlkspthlem2  26148  wwlknred  26251  wwlknext  26252  wwlkextwrd  26256  clwwlkel  26321  wwlkext2clwwlk  26331  clwlkfoclwwlk  26372  clwlkf1clwwlklem2  26374  el2spthonot  26397  vdgrnn0pnf  26436  rusgra0edg  26482  eupai  26494  frgrancvvdeqlem3  26559  frgrancvvdeqlemC  26566  frgrawopreg  26576  frg2woteqm  26586  frrusgraord  26598  extwwlkfablem2  26605  frgrareg  26644  grpoidinvlem1  26742  grporcan  26756  ipblnfi  27095  hvmulcan2  27314  shscli  27560  spansneleq  27813  pjspansn  27820  3oalem2  27906  eigposi  28079  cnlnadjlem2  28311  stlesi  28484  mdslmd1lem1  28568  mdslmd1lem2  28569  cdj1i  28676  disjxpin  28783  xreceu  28961  txomap  29229  pstmxmet  29268  qqhghm  29360  qqhrhm  29361  measinblem  29610  cntmeas  29616  ballotlemsf1o  29902  bnj945  30098  bnj1110  30304  cvmopnlem  30514  cvmfolem  30515  cvmliftmolem2  30518  cvmlift2lem10  30548  mrsubvrs  30673  poseq  30994  wzel  31015  wzelOLD  31016  sltres  31061  btwnconn1lem8  31371  btwnconn1lem9  31372  btwnconn1lem10  31373  btwnconn1lem11  31374  btwnconn1lem12  31375  finminlem  31482  nn0prpwlem  31487  fnessref  31522  refssfne  31523  fnemeet2  31532  consym1  31589  bj-finsumval0  32324  topdifinffinlem  32371  relowlssretop  32387  rdgeqoa  32394  matunitlindflem1  32575  poimirlem28  32607  mblfinlem1  32616  mblfinlem3  32618  mblfinlem4  32619  ovoliunnfl  32621  mbfresfi  32626  mbfposadd  32627  itg2addnclem2  32632  itg2addnc  32634  ftc1anc  32663  frinfm  32700  fdc  32711  blssp  32722  sstotbnd  32744  isbnd2  32752  ssbnd  32757  prdstotbnd  32763  prdsbnd2  32764  ismtyres  32777  heibor1lem  32778  rrnequiv  32804  rngoisocnv  32950  crngohomfo  32975  pridlc3  33042  prter3  33185  ax12eq  33244  ax12el  33245  cvratlem  33725  islvol2aN  33896  4atlem4b  33904  4atlem4c  33905  4atlem4d  33906  isline2  34078  isline3  34080  pclfinclN  34254  linepsubclN  34255  pexmidlem4N  34277  diaglbN  35362  dvhvaddcl  35402  dvhvaddcomN  35403  dvhvscacl  35410  djavalN  35442  dibglbN  35473  dihatexv  35645  djhval  35705  mapdrvallem2  35952  elrfi  36275  nacsfix  36293  eldioph2  36343  lzenom  36351  rexrabdioph  36376  irrapxlem3  36406  pellexlem5  36415  pellex  36417  pell1234qrne0  36435  pell1234qrmulcl  36437  pell14qrdich  36451  pell1qrge1  36452  pellqrex  36461  rmxypairf1o  36494  rmxycomplete  36500  monotoddzzfi  36525  congadd  36551  jm2.19lem3  36576  jm2.19lem4  36577  jm2.25  36584  jm2.26a  36585  jm2.26lem3  36586  expdiophlem1  36606  wepwsolem  36630  lmhmfgsplit  36674  aaitgo  36751  mon1psubm  36803  deg1mhm  36804  iunrelexp0  37013  isotone2  37367  disjrnmpt2  38370  mullimc  38683  mullimcf  38690  fprodcncf  38787  stoweidlem17  38910  stoweidlem27  38920  stoweidlem54  38947  fourierdlem42  39042  fourierdlem62  39061  fourierdlem73  39072  fourierdlem76  39075  fourierdlem97  39096  sge0iunmptlemfi  39306  isomenndlem  39420  ovnsslelem  39450  smonoord  39944  iccpartiltu  39960  fmtnoprmfac1  40015  prmdvdsfmtnof1lem2  40035  ccatpfx  40272  imarnf1pr  40326  subupgr  40511  nbgr0vtxlem  40577  nb3grprlem1  40608  cusgredg  40646  cusgrres  40664  usgredgsscusgredg  40675  1wlkl1loop  40842  1wlkp1lem4  40885  wwlksnred  41098  wwlksnext  41099  wwlksnextwrd  41103  wwlksnwwlksnon  41121  wpthswwlks2on  41164  clwwlksel  41221  wwlksext2clwwlk  41231  clwwnisshclwwsn  41237  clwlksfoclwwlk  41270  31wlkond  41338  1conngr  41361  eucrctshift  41411  frgrncvvdeqlem3  41471  frgrncvvdeqlemC  41478  frgrwopreglem3  41483  frgrwopreg  41486  frrusgrord  41504  av-numclwlk1lem2f1  41524  av-numclwwlkqhash  41530  mgmhmlin  41576  rnghmmul  41690  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  funcringcsetcALTV2lem9  41836  ringcinvALTV  41848  funcringcsetclem9ALTV  41859  mndpsuppss  41946  lmodvsmdi  41957  lincsum  42012  lindslinindimp2lem4  42044  nn0sumshdiglemB  42212
  Copyright terms: Public domain W3C validator