Theorem ad2antll 730

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

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 481	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜓)
3	2	adantl 481	1 ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simprr  773  simprrl  781  simprrr  782  simprr1  1223  simprr2  1224  simprr3  1225  prneimg  4811  prproe  4862  fr2nr  5602  wereu2  5622  f1oprg  6821  fvtp1g  7146  funfvima3  7184  isof1oidb  7272  isomin  7285  weniso  7302  elovmpt3rab1  7620  sorpssi  7676  resf1extb  7878  poseq  8102  suppofssd  8147  tfrlem9a  8319  oalimcl  8489  odi  8508  oeeui  8532  ralxpmap  8838  boxriin  8882  domdifsn  8992  domunsncan  9009  enfixsn  9018  disjen  9066  mapen  9073  mapxpen  9075  mapunen  9078  findcard2d  9095  unxpdomlem2  9161  unxpdomlem3  9162  isfinite2  9202  marypha1lem  9340  marypha2  9346  supmo  9359  infmo  9404  card2inf  9464  brwdom2  9482  wemapwe  9610  rankonidlem  9744  rankxplim3  9797  djulf1o  9828  djurf1o  9829  infxpenlem  9927  infxpenc2lem1  9933  infxpenc2  9936  fseqenlem1  9938  fseqenlem2  9939  infpwfien  9976  dfac12lem2  10059  infunsdom1  10126  infunsdom  10127  infmap2  10131  fin2i2  10232  fin23lem28  10254  fin23lem32  10258  fin23lem34  10260  fin23lem40  10265  isf32lem2  10268  compssiso  10288  isfin1-3  10300  fin1a2lem10  10323  fin12  10327  hsmexlem4  10343  ac6num  10393  ttukeylem7  10429  axdclem2  10434  iundom2g  10454  fpwwe2lem11  10556  pwfseqlem3  10575  winalim2  10611  winafp  10612  wunex2  10653  grur1  10735  dedekindle  11301  00id  11312  receu  11786  lt2mul2div  12024  peano5uzi  12585  uzwo  12828  qbtwnre  13118  iooshf  13346  modmul1  13851  seqcl2  13947  seqfveq2  13951  seqid2  13975  seqdistr  13980  expcl2lem  14000  mulexpz  14029  expnlbnd2  14161  hashfun  14364  hashfacen  14381  hashf1lem1  14382  elss2prb  14415  fstwrdne0  14483  swrdsb0eq  14591  swrdswrd  14632  wrd2ind  14650  swrdccatin1  14652  pfxccatin12  14660  splid  14680  repswrevw  14714  cshwidxmod  14730  cshwidx0  14733  2cshw  14740  cshweqrep  14748  cshw1  14749  wwlktovfo  14885  relexpfld  14976  relexpindlem  14990  01sqrexlem6  15174  absexpz  15232  o1rlimmul  15546  iseralt  15612  summolem2  15643  fsumf1o  15650  fsum0diag2  15710  fsummulc2  15711  cvgcmpce  15745  incexclem  15763  prodmolem2  15862  fprodcl2lem  15877  fprodmul  15887  fprodrev  15904  moddvds  16194  dvdsflip  16248  bitsf1ocnv  16375  sadcaddlem  16388  bezoutlem2  16471  bezoutlem4  16473  dfgcd2  16477  lcmgcdlem  16537  crth  16709  hashgcdlem  16719  phisum  16722  pcqcl  16788  pcid  16805  pcneg  16806  prmpwdvds  16836  pockthg  16838  4sqlem11  16887  ramub2  16946  0ram  16952  prmgaplem7  16989  prmgaplem8  16990  setscom  17111  qusval  17467  initoeu1  17939  termoeu1  17946  setcinv  18018  funcestrcsetclem9  18075  funcsetcestrclem9  18090  fullsetcestrc  18093  1stfcl  18124  2ndfcl  18125  hofpropd  18194  isacs3lem  18469  mgmhmlin  18628  mndpsuppss  18694  frmdss2  18792  frmdup1  18793  mgm2nsgrplem2  18848  mulgdirlem  19039  mulgass  19045  0nsg  19102  cycsubgcl  19139  ghmmulg  19161  conjghm  19182  qusghm  19188  gsumwrev  19299  symg2bas  19326  symgfixelsi  19368  f1otrspeq  19380  psgnunilem2  19428  psgnunilem3  19429  odf1o2  19506  lsmhash  19638  efgtf  19655  efginvrel2  19660  efgredeu  19685  efgcpbllemb  19688  frgpuplem  19705  frgpup1  19708  ghmcyg  19829  gsumval3lem1  19838  gsumzres  19842  gsumzcl2  19843  gsumzf1o  19845  gsumzaddlem  19854  gsumconst  19867  gsumzmhm  19870  gsumzoppg  19877  gsum2d  19905  subgdmdprd  19969  pgpfac1lem3  20012  gsummgp0  20257  rnghmmul  20389  rngcinv  20574  ringcinv  20608  islmodd  20821  lmodvsmmulgdi  20852  islss3  20914  0lmhm  20996  idlmhm  20997  lmhmeql  21011  pwssplit3  21017  lidldvgen  21293  qsssubdrg  21385  cnsubrg  21386  znf1o  21510  psgnghm  21539  psgndif  21561  cssmre  21652  dsmmsubg  21702  frlmup1  21757  lindfrn  21780  f1lindf  21781  evlslem1  22041  psdmul  22113  coe1tmmul2  22222  pf1ind  22303  mamufval  22340  mamurid  22390  mvmulfval  22490  mdetralt2  22557  mndifsplit  22584  maducoeval2  22588  madugsum  22591  mat2pmatmul  22679  decpmatmul  22720  pm2mpf1lem  22742  pm2mpf1  22747  monmat2matmon  22772  chpscmat  22790  fvmptnn04if  22797  tgcl  22917  ppttop  22955  epttop  22957  clsval2  22998  opncldf1  23032  mretopd  23040  neindisj  23065  neiptopnei  23080  restcls  23129  restntr  23130  ordtbas  23140  cnpnei  23212  cncls2  23221  tgcmp  23349  cmpcld  23350  uncmp  23351  hauscmplem  23354  1stcfb  23393  2ndcctbss  23403  hauspwdom  23449  reftr  23462  comppfsc  23480  kgentopon  23486  ptpjpre1  23519  ptcnplem  23569  txcn  23574  txdis1cn  23583  txhaus  23595  xkopt  23603  imasnopn  23638  imasncld  23639  imasncls  23640  hmeoimaf1o  23718  cmphaushmeo  23748  txhmeo  23751  trfbas2  23791  fbasfip  23816  fbasrn  23832  fmss  23894  elfm2  23896  hauspwpwf1  23935  flfcnp  23952  fclscf  23973  flimfnfcls  23976  fcfval  23981  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALTlem4  23998  ptcmplem3  24002  ptcmplem4  24003  cnextfval  24010  cnextcn  24015  tmdgsum2  24044  ustex2sym  24165  neipcfilu  24243  imasdsf1olem  24321  metss2lem  24459  stdbdxmet  24463  stdbdmopn  24466  metrest  24472  metcnp  24489  restmetu  24518  tngngp  24602  icccmplem1  24771  icccvx  24908  evth  24918  lebnumlem1  24920  pi1blem  24999  isncvsngp  25109  equivcau  25260  bcthlem5  25288  cmslssbn  25332  ivthlem3  25414  ovolicc2lem3  25480  ovolicc2lem4  25481  dyaddisj  25557  dyadmbllem  25560  ismbfd  25600  itg2seq  25703  itgss  25773  limciun  25855  dvcobr  25909  dvcobrOLD  25910  dvmptfsum  25939  c1liplem1  25961  c1lip1  25962  lhop  25981  dvcvx  25985  tdeglem4  26025  plyco0  26157  elply2  26161  plypf1  26177  dgreq0  26231  elqaalem2  26288  aalioulem6  26305  aaliou  26306  aaliou2b  26309  ulmss  26366  ulmcn  26368  pserulm  26391  lgamgulmlem5  27003  basellem4  27054  fsumdvdsdiaglem  27153  mpodvdsmulf1o  27164  dvdsmulf1o  27166  chtublem  27182  fsumvma2  27185  logfaclbnd  27193  dchrelbasd  27210  lgsqrlem2  27318  gausslemma2dlem1a  27336  lgseisenlem2  27347  lgsquadlem1  27351  lgsquadlem2  27352  lgsquadlem3  27353  rplogsumlem2  27456  rpvmasumlem  27458  dchrmusum2  27465  dchrvmasumlem1  27466  dchrvmasum2lem  27467  rpvmasum2  27483  dchrisum0lem1  27487  logsqvma  27513  selberg4  27532  pntibndlem3  27563  pntlem3  27580  ostthlem1  27598  ostthlem2  27599  sltres  27634  nogt01o  27668  oldbdayim  27871  addsproplem2  27952  negsproplem2  28011  mulsval  28091  om2noseqrdg  28285  noseqrdgfn  28287  zmulscld  28376  recut  28473  idmot  28592  brcgr  28956  brbtwn2  28961  axsegconlem8  28980  axpaschlem  28996  axeuclid  29019  axcontlem2  29021  axcontlem7  29026  eengtrkg  29042  upgrex  29148  subgrprop3  29332  subupgr  29343  nbgr0edglem  29412  nb3grprlem1  29436  cusgredg  29480  cusgrres  29505  usgredgsscusgredg  29516  finsumvtxdg2ssteplem4  29605  finsumvtxdg2sstep  29606  wlkl1loop  29694  wlkp1lem4  29731  wwlksnred  29948  wwlksnext  29949  wwlksnextwrd  29953  wpthswwlks2on  30020  clwwlknp  30095  clwwlkel  30104  wwlksext2clwwlk  30115  clwwlknonwwlknonb  30164  3wlkond  30229  1conngr  30252  eucrctshift  30301  fusgr2wsp2nb  30392  numclwwlk1lem2foa  30412  numclwwlk1lem2f1  30415  numclwlk1lem1  30427  numclwlk1lem2  30428  grpoidinvlem1  30562  grporcan  30576  ipblnfi  30913  hvmulcan2  31131  shscli  31375  spansneleq  31628  pjspansn  31635  3oalem2  31721  eigposi  31894  cnlnadjlem2  32126  stlesi  32299  mdslmd1lem1  32383  mdslmd1lem2  32384  cdj1i  32491  disjxpin  32645  nn0xmulclb  32832  xreceu  32984  txomap  33972  pstmxmet  34035  qqhghm  34126  qqhrhm  34127  measinblem  34358  cntmeas  34364  ballotlemsf1o  34652  bnj945  34910  bnj1110  35119  f1resveqaeq  35222  rankfilimbi  35238  cvmopnlem  35453  cvmfolem  35454  cvmliftmolem2  35457  cvmlift2lem10  35487  satf00  35549  satffunlem2lem1  35579  satefvfmla0  35593  mrsubvrs  35697  wzel  35997  btwnconn1lem8  36269  btwnconn1lem9  36270  btwnconn1lem10  36271  btwnconn1lem11  36272  btwnconn1lem12  36273  finminlem  36493  nn0prpwlem  36497  fnessref  36532  refssfne  36533  fnemeet2  36542  consym1  36595  bj-finsumval0  37461  topdifinffinlem  37523  relowlssretop  37539  rdgeqoa  37546  fvineqsneu  37587  pibt2  37593  matunitlindflem1  37788  poimirlem28  37820  mblfinlem1  37829  mblfinlem3  37831  mblfinlem4  37832  ovoliunnfl  37834  mbfresfi  37838  mbfposadd  37839  itg2addnclem2  37844  itg2addnc  37846  ftc1anc  37873  frinfm  37907  fdc  37917  blssp  37928  sstotbnd  37947  isbnd2  37955  ssbnd  37960  prdstotbnd  37966  prdsbnd2  37967  ismtyres  37980  heibor1lem  37981  rrnequiv  38007  rngoisocnv  38153  crngohomfo  38178  pridlc3  38245  membpartlem19  39086  prter3  39179  ax12eq  39238  ax12el  39239  cvratlem  39718  islvol2aN  39889  4atlem4b  39897  4atlem4c  39898  4atlem4d  39899  isline2  40071  isline3  40073  pclfinclN  40247  linepsubclN  40248  pexmidlem4N  40270  diaglbN  41352  dvhvaddcl  41392  dvhvaddcomN  41393  dvhvscacl  41400  djavalN  41432  dibglbN  41463  dihatexv  41635  djhval  41695  mapdrvallem2  41942  evlselvlem  42865  evlselv  42866  mhpind  42873  prjsprellsp  42890  elrfi  42972  nacsfix  42990  eldioph2  43040  lzenom  43048  rexrabdioph  43072  irrapxlem3  43102  pellexlem5  43111  pellex  43113  pell1234qrne0  43131  pell1234qrmulcl  43133  pell14qrdich  43147  pell1qrge1  43148  pellqrex  43157  rmxypairf1o  43189  rmxycomplete  43195  monotoddzzfi  43220  congadd  43244  jm2.19lem3  43269  jm2.19lem4  43270  jm2.25  43277  jm2.26a  43278  jm2.26lem3  43279  expdiophlem1  43299  wepwsolem  43320  lmhmfgsplit  43364  aaitgo  43440  mon1psubm  43477  deg1mhm  43478  succlg  43606  ofoacom  43639  iunrelexp0  43979  isotone2  44326  mnuprdlem4  44552  relpmin  45229  disjrnmpt2  45468  mullimc  45898  mullimcf  45905  climxrre  46030  fprodcncf  46180  stoweidlem17  46297  stoweidlem27  46307  stoweidlem54  46334  fourierdlem42  46429  fourierdlem62  46448  fourierdlem73  46459  fourierdlem76  46462  fourierdlem97  46483  sge0iunmptlemfi  46693  isomenndlem  46810  imarnf1pr  47564  smonoord  47653  fvelsetpreimafv  47669  iccpartiltu  47704  sprsymrelf1lem  47773  prproropf1olem3  47787  paireqne  47793  fmtnoprmfac1  47847  prmdvdsfmtnof1lem2  47867  gricushgr  48199  grimedg  48217  cycl3grtri  48229  gpgedg2iv  48349  pgnbgreunbgrlem2lem1  48396  pgnbgreunbgrlem2lem2  48397  rngcinvALTV  48558  funcringcsetcALTV2lem9  48580  ringcinvALTV  48592  funcringcsetclem9ALTV  48603  lmodvsmdi  48661  lincsum  48711  lindslinindimp2lem4  48743  nn0sumshdiglemB  48902  1arymaptf1  48924  2arymaptf1  48935  dmrnxp  49118  xpco2  49138  initopropd  49524  termopropd  49525  zeroopropd  49526  oduoppcciso  49847  lanpropd  49896  ranpropd  49897