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

Theorem ad2antll 760
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 480 . 2 ((𝜃𝜑) → 𝜓)
32adantl 480 1 ((𝜒 ∧ (𝜃𝜑)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  simprr  791  simprrl  799  simprrr  800  prneimg  4323  fr2nr  5005  wereu2  5024  f1oprg  6077  fvtp1g  6345  funfvima3  6376  isof1oidb  6451  isomin  6464  weniso  6481  elovmpt3rab1  6768  sorpssi  6818  tfrlem9a  7346  oalimcl  7504  odi  7523  oeeui  7546  ralxpmap  7770  boxriin  7813  domdifsn  7905  domunsncan  7922  enfixsn  7931  disjen  7979  mapen  7986  mapxpen  7988  mapunen  7991  unxpdomlem2  8027  unxpdomlem3  8028  findcard2d  8064  findcard3  8065  isfinite2  8080  marypha1lem  8199  marypha2  8205  supmo  8218  infmo  8261  card2inf  8320  brwdom2  8338  wemapwe  8454  rankonidlem  8551  rankxplim3  8604  infxpenlem  8696  infxpenc2lem1  8702  infxpenc2  8705  fseqenlem1  8707  fseqenlem2  8708  infpwfien  8745  dfac12lem2  8826  infunsdom1  8895  infunsdom  8896  infmap2  8900  fin2i2  9000  fin23lem28  9022  fin23lem32  9026  fin23lem34  9028  fin23lem40  9033  isf32lem2  9036  compssiso  9056  isfin1-3  9068  fin1a2lem10  9091  fin12  9095  hsmexlem4  9111  ac6num  9161  ttukeylem7  9197  axdclem2  9202  iundom2g  9218  fpwwe2lem12  9319  pwfseqlem3  9338  winalim2  9374  winafp  9375  wunex2  9416  grur1  9498  dedekindle  10052  00id  10062  receu  10523  lt2mul2div  10752  peano5uzi  11300  uzwo  11585  qbtwnre  11865  iooshf  12081  modmul1  12542  seqcl2  12638  seqfveq2  12642  seqid2  12666  seqdistr  12671  expcl2lem  12691  mulexpz  12719  expnlbnd2  12814  hashfun  13038  hashfacen  13049  hashf1lem1  13050  elss2prb  13075  fstwrdne0  13148  swrdswrd  13260  wrd2ind  13277  splid  13303  repswrevw  13332  cshwidx0  13351  2cshw  13358  cshweqrep  13366  cshw1  13367  wwlktovfo  13497  relexpfld  13585  relexpindlem  13599  sqrlem6  13784  absexpz  13841  o1rlimmul  14145  iseralt  14211  summolem2  14242  fsumf1o  14249  fsum0diag2  14305  fsummulc2  14306  cvgcmpce  14339  incexclem  14355  prodmolem2  14452  fprodcl2lem  14467  fprodmul  14477  fprodrev  14494  moddvds  14777  dvdsflip  14825  bitsf1ocnv  14952  sadcaddlem  14965  bezoutlem2  15043  bezoutlem4  15045  dfgcd2  15049  lcmgcdlem  15105  crth  15269  hashgcdlem  15279  phisum  15281  pcqcl  15347  pcid  15363  pcneg  15364  prmpwdvds  15394  pockthg  15396  4sqlem11  15445  ramub2  15504  0ram  15510  prmgaplem7  15547  prmgaplem8  15548  setscom  15679  qusval  15973  initoeu1  16432  termoeu1  16439  setcinv  16511  funcestrcsetclem9  16559  funcsetcestrclem9  16574  fullsetcestrc  16577  1stfcl  16608  2ndfcl  16609  hofpropd  16678  isacs3lem  16937  frmdss2  17171  frmdup1  17172  mgm2nsgrplem2  17177  mulgdirlem  17343  mulgass  17350  cycsubgcl  17391  0nsg  17410  ghmmulg  17443  conjghm  17462  qusghm  17468  gsumwrev  17567  symg2bas  17589  symgfixelsi  17626  f1otrspeq  17638  psgnunilem2  17686  psgnunilem3  17687  odf1o2  17759  lsmhash  17889  efgtf  17906  efgredeu  17936  efgcpbllemb  17939  frgpuplem  17956  frgpup1  17959  cygabl  18063  ghmcyg  18068  gsumval3lem1  18077  gsumzres  18081  gsumzcl2  18082  gsumzf1o  18084  gsumzaddlem  18092  gsumconst  18105  gsumzmhm  18108  gsumzoppg  18115  gsum2d  18142  subgdmdprd  18204  pgpfac1lem3  18247  gsummgp0  18379  islmodd  18640  islss3  18728  0lmhm  18809  idlmhm  18810  lmhmeql  18824  pwssplit3  18830  lidldvgen  19024  evlslem1  19284  coe1tmmul2  19415  pf1ind  19488  qsssubdrg  19572  cnsubrg  19573  znf1o  19666  psgnghm  19692  psgndif  19714  cssmre  19803  dsmmsubg  19853  frlmup1  19903  lindfrn  19926  f1lindf  19927  mamufval  19957  mamurid  20014  mvmulfval  20114  mdetralt2  20181  mndifsplit  20208  maducoeval2  20212  madugsum  20215  mat2pmatmul  20302  decpmatmul  20343  pm2mpf1lem  20365  pm2mpf1  20370  monmat2matmon  20395  chpscmat  20413  fvmptnn04if  20420  tgcl  20531  ppttop  20568  epttop  20570  clsval2  20611  opncldf1  20645  mretopd  20653  neindisj  20678  neiptopnei  20693  restcls  20742  restntr  20743  ordtbas  20753  cnpnei  20825  cncls2  20834  tgcmp  20961  cmpcld  20962  uncmp  20963  hauscmplem  20966  1stcfb  21005  2ndcctbss  21015  hauspwdom  21061  reftr  21074  comppfsc  21092  kgentopon  21098  ptpjpre1  21131  ptcnplem  21181  txcn  21186  txdis1cn  21195  txhaus  21207  xkopt  21215  imasnopn  21250  imasncld  21251  imasncls  21252  hmeoimaf1o  21330  cmphaushmeo  21360  txhmeo  21363  trfbas2  21404  fbasfip  21429  fbasrn  21445  fmss  21507  elfm2  21509  hauspwpwf1  21548  flfcnp  21565  fclscf  21586  flimfnfcls  21589  fcfval  21594  alexsubALTlem2  21609  alexsubALTlem3  21610  alexsubALTlem4  21611  ptcmplem3  21615  ptcmplem4  21616  cnextfval  21623  cnextcn  21628  tmdgsum2  21657  ustex2sym  21777  neipcfilu  21857  imasdsf1olem  21935  metss2lem  22073  stdbdxmet  22077  stdbdmopn  22080  metrest  22086  metcnp  22103  restmetu  22132  tngngp  22215  icccmplem1  22380  icccvx  22504  evth  22513  lebnumlem1  22515  pi1blem  22594  isncvsngp  22701  equivcau  22850  bcthlem5  22877  ivthlem3  22973  ovolicc2lem3  23038  ovolicc2lem4  23039  dyaddisj  23114  dyadmbllem  23117  ismbfd  23157  itg2seq  23259  itgss  23328  limciun  23408  dvcobr  23459  dvmptfsum  23486  c1liplem1  23507  c1lip1  23508  lhop  23527  dvcvx  23531  plyco0  23696  elply2  23700  plypf1  23716  dgreq0  23769  elqaalem2  23823  aalioulem6  23840  aaliou  23841  aaliou2b  23844  ulmss  23899  ulmcn  23901  pserulm  23924  lgamgulmlem5  24503  basellem4  24554  fsumdvdsdiaglem  24653  dvdsmulf1o  24664  chtublem  24680  fsumvma2  24683  logfaclbnd  24691  dchrelbasd  24708  lgsqrlem2  24816  gausslemma2dlem1a  24834  lgseisenlem2  24845  lgsquadlem1  24849  lgsquadlem2  24850  lgsquadlem3  24851  rplogsumlem2  24918  rpvmasumlem  24920  dchrmusum2  24927  dchrvmasumlem1  24928  dchrvmasum2lem  24929  rpvmasum2  24945  dchrisum0lem1  24949  logsqvma  24975  selberg4  24994  pntibndlem3  25025  pntlem3  25042  ostthlem1  25060  ostthlem2  25061  idmot  25177  brcgr  25525  brbtwn2  25530  axsegconlem8  25549  axpaschlem  25565  axeuclid  25588  axcontlem2  25590  axcontlem7  25595  eengtrkg  25610  umgraex  25645  nbgraf1olem5  25767  nb3graprlem1  25773  usgrasscusgra  25804  wlks  25840  usgra2wlkspthlem2  25941  wwlknred  26044  wwlknext  26045  wwlkextwrd  26049  clwwlkel  26114  wwlkext2clwwlk  26124  clwlkfoclwwlk  26165  clwlkf1clwwlklem2  26167  el2spthonot  26190  vdgrnn0pnf  26229  rusgra0edg  26275  eupai  26287  frgrancvvdeqlem3  26352  frgrancvvdeqlemC  26359  frgrawopreg  26369  frg2woteqm  26379  frrusgraord  26391  extwwlkfablem2  26398  frgrareg  26437  grpoidinvlem1  26535  grporcan  26549  ipblnfi  26888  hvmulcan2  27107  shscli  27353  spansneleq  27606  pjspansn  27613  3oalem2  27699  eigposi  27872  cnlnadjlem2  28104  stlesi  28277  mdslmd1lem1  28361  mdslmd1lem2  28362  cdj1i  28469  disjxpin  28576  xreceu  28754  txomap  29022  pstmxmet  29061  qqhghm  29153  qqhrhm  29154  measinblem  29403  cntmeas  29409  ballotlemsf1o  29695  bnj945  29891  bnj1110  30097  cvmopnlem  30307  cvmfolem  30308  cvmliftmolem2  30311  cvmlift2lem10  30341  mrsubvrs  30466  poseq  30787  wzel  30808  wzelOLD  30809  sltres  30854  btwnconn1lem8  31164  btwnconn1lem9  31165  btwnconn1lem10  31166  btwnconn1lem11  31167  btwnconn1lem12  31168  finminlem  31275  nn0prpwlem  31280  fnessref  31315  refssfne  31316  fnemeet2  31325  consym1  31382  bj-finsumval0  32107  topdifinffinlem  32154  relowlssretop  32170  rdgeqoa  32177  matunitlindflem1  32358  poimirlem28  32390  mblfinlem1  32399  mblfinlem3  32401  mblfinlem4  32402  ovoliunnfl  32404  mbfresfi  32409  mbfposadd  32410  itg2addnclem2  32415  itg2addnc  32417  ftc1anc  32446  frinfm  32483  fdc  32494  blssp  32505  sstotbnd  32527  isbnd2  32535  ssbnd  32540  prdstotbnd  32546  prdsbnd2  32547  ismtyres  32560  heibor1lem  32561  rrnequiv  32587  rngoisocnv  32733  crngohomfo  32758  pridlc3  32825  prter3  32968  ax12eq  33027  ax12el  33028  cvratlem  33508  islvol2aN  33679  4atlem4b  33687  4atlem4c  33688  4atlem4d  33689  isline2  33861  isline3  33863  pclfinclN  34037  linepsubclN  34038  pexmidlem4N  34060  diaglbN  35145  dvhvaddcl  35185  dvhvaddcomN  35186  dvhvscacl  35193  djavalN  35225  dibglbN  35256  dihatexv  35428  djhval  35488  mapdrvallem2  35735  elrfi  36058  nacsfix  36076  eldioph2  36126  lzenom  36134  rexrabdioph  36159  irrapxlem3  36189  pellexlem5  36198  pellex  36200  pell1234qrne0  36218  pell1234qrmulcl  36220  pell14qrdich  36234  pell1qrge1  36235  pellqrex  36244  rmxypairf1o  36277  rmxycomplete  36283  monotoddzzfi  36308  congadd  36334  jm2.19lem3  36359  jm2.19lem4  36360  jm2.25  36367  jm2.26a  36368  jm2.26lem3  36369  expdiophlem1  36389  wepwsolem  36413  lmhmfgsplit  36457  aaitgo  36534  mon1psubm  36586  deg1mhm  36587  iunrelexp0  36796  isotone2  37150  disjrnmpt2  38153  mullimc  38466  mullimcf  38473  fprodcncf  38570  stoweidlem17  38693  stoweidlem27  38703  stoweidlem54  38730  fourierdlem42  38825  fourierdlem62  38844  fourierdlem73  38855  fourierdlem76  38858  fourierdlem97  38879  sge0iunmptlemfi  39089  isomenndlem  39203  ovnsslelem  39233  smonoord  39728  iccpartiltu  39744  fmtnoprmfac1  39799  prmdvdsfmtnof1lem2  39819  ccatpfx  40056  imarnf1pr  40121  upgrex  40299  subupgr  40492  nbgr0vtxlem  40558  nb3grprlem1  40589  cusgredg  40627  cusgrres  40645  usgredgsscusgredg  40656  1wlkl1loop  40823  1wlkp1lem4  40866  wwlksnred  41079  wwlksnext  41080  wwlksnextwrd  41084  wwlksnwwlksnon  41102  wpthswwlks2on  41145  clwwlksel  41202  wwlksext2clwwlk  41212  clwwnisshclwwsn  41218  clwlksfoclwwlk  41251  31wlkond  41319  1conngr  41342  eucrctshift  41392  frgrncvvdeqlem3  41452  frgrncvvdeqlemC  41459  frgrwopreglem3  41464  frgrwopreg  41467  frrusgrord  41485  av-numclwlk1lem2f1  41505  av-numclwwlkqhash  41511  mgmhmlin  41557  rnghmmul  41671  rngcinv  41754  rngcinvALTV  41766  ringcinv  41805  funcringcsetcALTV2lem9  41817  ringcinvALTV  41829  funcringcsetclem9ALTV  41840  mndpsuppss  41927  lmodvsmdi  41938  lincsum  41993  lindslinindimp2lem4  42025  nn0sumshdiglemB  42193
  Copyright terms: Public domain W3C validator