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  4797  prproe  4848  fr2nr  5608  wereu2  5628  f1oprg  6826  fvtp1g  7153  funfvima3  7191  isof1oidb  7279  isomin  7292  weniso  7309  elovmpt3rab1  7627  sorpssi  7683  resf1extb  7885  poseq  8108  suppofssd  8153  tfrlem9a  8325  oalimcl  8495  odi  8514  oeeui  8538  ralxpmap  8844  boxriin  8888  domdifsn  8998  domunsncan  9015  enfixsn  9024  disjen  9072  mapen  9079  mapxpen  9081  mapunen  9084  findcard2d  9101  unxpdomlem2  9167  unxpdomlem3  9168  isfinite2  9208  marypha1lem  9346  marypha2  9352  supmo  9365  infmo  9410  card2inf  9470  brwdom2  9488  wemapwe  9618  rankonidlem  9752  rankxplim3  9805  djulf1o  9836  djurf1o  9837  infxpenlem  9935  infxpenc2lem1  9941  infxpenc2  9944  fseqenlem1  9946  fseqenlem2  9947  infpwfien  9984  dfac12lem2  10067  infunsdom1  10134  infunsdom  10135  infmap2  10139  fin2i2  10240  fin23lem28  10262  fin23lem32  10266  fin23lem34  10268  fin23lem40  10273  isf32lem2  10276  compssiso  10296  isfin1-3  10308  fin1a2lem10  10331  fin12  10335  hsmexlem4  10351  ac6num  10401  ttukeylem7  10437  axdclem2  10442  iundom2g  10462  fpwwe2lem11  10564  pwfseqlem3  10583  winalim2  10619  winafp  10620  wunex2  10661  grur1  10743  dedekindle  11310  00id  11321  receu  11795  lt2mul2div  12034  peano5uzi  12618  uzwo  12861  qbtwnre  13151  iooshf  13379  modmul1  13886  seqcl2  13982  seqfveq2  13986  seqid2  14010  seqdistr  14015  expcl2lem  14035  mulexpz  14064  expnlbnd2  14196  hashfun  14399  hashfacen  14416  hashf1lem1  14417  elss2prb  14450  fstwrdne0  14518  swrdsb0eq  14626  swrdswrd  14667  wrd2ind  14685  swrdccatin1  14687  pfxccatin12  14695  splid  14715  repswrevw  14749  cshwidxmod  14765  cshwidx0  14768  2cshw  14775  cshweqrep  14783  cshw1  14784  wwlktovfo  14920  relexpfld  15011  relexpindlem  15025  01sqrexlem6  15209  absexpz  15267  o1rlimmul  15581  iseralt  15647  summolem2  15678  fsumf1o  15685  fsum0diag2  15745  fsummulc2  15746  cvgcmpce  15781  incexclem  15801  prodmolem2  15900  fprodcl2lem  15915  fprodmul  15925  fprodrev  15942  moddvds  16232  dvdsflip  16286  bitsf1ocnv  16413  sadcaddlem  16426  bezoutlem2  16509  bezoutlem4  16511  dfgcd2  16515  lcmgcdlem  16575  crth  16748  hashgcdlem  16758  phisum  16761  pcqcl  16827  pcid  16844  pcneg  16845  prmpwdvds  16875  pockthg  16877  4sqlem11  16926  ramub2  16985  0ram  16991  prmgaplem7  17028  prmgaplem8  17029  setscom  17150  qusval  17506  initoeu1  17978  termoeu1  17985  setcinv  18057  funcestrcsetclem9  18114  funcsetcestrclem9  18129  fullsetcestrc  18132  1stfcl  18163  2ndfcl  18164  hofpropd  18233  isacs3lem  18508  mgmhmlin  18667  mndpsuppss  18733  frmdss2  18831  frmdup1  18832  mgm2nsgrplem2  18890  mulgdirlem  19081  mulgass  19087  0nsg  19144  cycsubgcl  19181  ghmmulg  19203  conjghm  19224  qusghm  19230  gsumwrev  19341  symg2bas  19368  symgfixelsi  19410  f1otrspeq  19422  psgnunilem2  19470  psgnunilem3  19471  odf1o2  19548  lsmhash  19680  efgtf  19697  efginvrel2  19702  efgredeu  19727  efgcpbllemb  19730  frgpuplem  19747  frgpup1  19750  ghmcyg  19871  gsumval3lem1  19880  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsumzoppg  19919  gsum2d  19947  subgdmdprd  20011  pgpfac1lem3  20054  gsummgp0  20297  rnghmmul  20429  rngcinv  20614  ringcinv  20648  islmodd  20861  lmodvsmmulgdi  20892  islss3  20954  0lmhm  21035  idlmhm  21036  lmhmeql  21050  pwssplit3  21056  lidldvgen  21332  qsssubdrg  21406  cnsubrg  21407  znf1o  21531  psgnghm  21560  psgndif  21582  cssmre  21673  dsmmsubg  21723  frlmup1  21778  lindfrn  21801  f1lindf  21802  evlslem1  22060  psdmul  22132  coe1tmmul2  22241  pf1ind  22320  mamufval  22357  mamurid  22407  mvmulfval  22507  mdetralt2  22574  mndifsplit  22601  maducoeval2  22605  madugsum  22608  mat2pmatmul  22696  decpmatmul  22737  pm2mpf1lem  22759  pm2mpf1  22764  monmat2matmon  22789  chpscmat  22807  fvmptnn04if  22814  tgcl  22934  ppttop  22972  epttop  22974  clsval2  23015  opncldf1  23049  mretopd  23057  neindisj  23082  neiptopnei  23097  restcls  23146  restntr  23147  ordtbas  23157  cnpnei  23229  cncls2  23238  tgcmp  23366  cmpcld  23367  uncmp  23368  hauscmplem  23371  1stcfb  23410  2ndcctbss  23420  hauspwdom  23466  reftr  23479  comppfsc  23497  kgentopon  23503  ptpjpre1  23536  ptcnplem  23586  txcn  23591  txdis1cn  23600  txhaus  23612  xkopt  23620  imasnopn  23655  imasncld  23656  imasncls  23657  hmeoimaf1o  23735  cmphaushmeo  23765  txhmeo  23768  trfbas2  23808  fbasfip  23833  fbasrn  23849  fmss  23911  elfm2  23913  hauspwpwf1  23952  flfcnp  23969  fclscf  23990  flimfnfcls  23993  fcfval  23998  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem3  24019  ptcmplem4  24020  cnextfval  24027  cnextcn  24032  tmdgsum2  24061  ustex2sym  24182  neipcfilu  24260  imasdsf1olem  24338  metss2lem  24476  stdbdxmet  24480  stdbdmopn  24483  metrest  24489  metcnp  24506  restmetu  24535  tngngp  24619  icccmplem1  24788  icccvx  24917  evth  24926  lebnumlem1  24928  pi1blem  25006  isncvsngp  25116  equivcau  25267  bcthlem5  25295  cmslssbn  25339  ivthlem3  25420  ovolicc2lem3  25486  ovolicc2lem4  25487  dyaddisj  25563  dyadmbllem  25566  ismbfd  25606  itg2seq  25709  itgss  25779  limciun  25861  dvcobr  25913  dvmptfsum  25942  c1liplem1  25963  c1lip1  25964  lhop  25983  dvcvx  25987  tdeglem4  26025  plyco0  26157  elply2  26161  plypf1  26177  dgreq0  26230  elqaalem2  26286  aalioulem6  26303  aaliou  26304  aaliou2b  26307  ulmss  26362  ulmcn  26364  pserulm  26387  lgamgulmlem5  26996  basellem4  27047  fsumdvdsdiaglem  27146  mpodvdsmulf1o  27157  dvdsmulf1o  27159  chtublem  27174  fsumvma2  27177  logfaclbnd  27185  dchrelbasd  27202  lgsqrlem2  27310  gausslemma2dlem1a  27328  lgseisenlem2  27339  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  rplogsumlem2  27448  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  rpvmasum2  27475  dchrisum0lem1  27479  logsqvma  27505  selberg4  27524  pntibndlem3  27555  pntlem3  27572  ostthlem1  27590  ostthlem2  27591  ltsres  27626  nogt01o  27660  oldbdayim  27881  addsproplem2  27962  negsproplem2  28021  mulsval  28101  om2noseqrdg  28296  noseqrdgfn  28298  zmulscld  28389  recut  28486  idmot  28605  brcgr  28969  brbtwn2  28974  axsegconlem8  28993  axpaschlem  29009  axeuclid  29032  axcontlem2  29034  axcontlem7  29039  eengtrkg  29055  upgrex  29161  subgrprop3  29345  subupgr  29356  nbgr0edglem  29425  nb3grprlem1  29449  cusgredg  29493  cusgrres  29517  usgredgsscusgredg  29528  finsumvtxdg2ssteplem4  29617  finsumvtxdg2sstep  29618  wlkl1loop  29706  wlkp1lem4  29743  wwlksnred  29960  wwlksnext  29961  wwlksnextwrd  29965  wpthswwlks2on  30032  clwwlknp  30107  clwwlkel  30116  wwlksext2clwwlk  30127  clwwlknonwwlknonb  30176  3wlkond  30241  1conngr  30264  eucrctshift  30313  fusgr2wsp2nb  30404  numclwwlk1lem2foa  30424  numclwwlk1lem2f1  30427  numclwlk1lem1  30439  numclwlk1lem2  30440  grpoidinvlem1  30575  grporcan  30589  ipblnfi  30926  hvmulcan2  31144  shscli  31388  spansneleq  31641  pjspansn  31648  3oalem2  31734  eigposi  31907  cnlnadjlem2  32139  stlesi  32312  mdslmd1lem1  32396  mdslmd1lem2  32397  cdj1i  32504  disjxpin  32658  nn0xmulclb  32844  xreceu  32981  txomap  33978  pstmxmet  34041  qqhghm  34132  qqhrhm  34133  measinblem  34364  cntmeas  34370  ballotlemsf1o  34658  bnj945  34916  bnj1110  35124  f1resveqaeq  35228  rankfilimbi  35244  cvmopnlem  35460  cvmfolem  35461  cvmliftmolem2  35464  cvmlift2lem10  35494  satf00  35556  satffunlem2lem1  35586  satefvfmla0  35600  mrsubvrs  35704  wzel  36004  btwnconn1lem8  36276  btwnconn1lem9  36277  btwnconn1lem10  36278  btwnconn1lem11  36279  btwnconn1lem12  36280  finminlem  36500  nn0prpwlem  36504  fnessref  36539  refssfne  36540  fnemeet2  36549  consym1  36602  bj-finsumval0  37599  topdifinffinlem  37663  relowlssretop  37679  rdgeqoa  37686  fvineqsneu  37727  pibt2  37733  matunitlindflem1  37937  poimirlem28  37969  mblfinlem1  37978  mblfinlem3  37980  mblfinlem4  37981  ovoliunnfl  37983  mbfresfi  37987  mbfposadd  37988  itg2addnclem2  37993  itg2addnc  37995  ftc1anc  38022  frinfm  38056  fdc  38066  blssp  38077  sstotbnd  38096  isbnd2  38104  ssbnd  38109  prdstotbnd  38115  prdsbnd2  38116  ismtyres  38129  heibor1lem  38130  rrnequiv  38156  rngoisocnv  38302  crngohomfo  38327  pridlc3  38394  membpartlem19  39235  prter3  39328  ax12eq  39387  ax12el  39388  cvratlem  39867  islvol2aN  40038  4atlem4b  40046  4atlem4c  40047  4atlem4d  40048  isline2  40220  isline3  40222  pclfinclN  40396  linepsubclN  40397  pexmidlem4N  40419  diaglbN  41501  dvhvaddcl  41541  dvhvaddcomN  41542  dvhvscacl  41549  djavalN  41581  dibglbN  41612  dihatexv  41784  djhval  41844  mapdrvallem2  42091  evlselvlem  43019  evlselv  43020  mhpind  43027  prjsprellsp  43044  elrfi  43126  nacsfix  43144  eldioph2  43194  lzenom  43202  rexrabdioph  43222  irrapxlem3  43252  pellexlem5  43261  pellex  43263  pell1234qrne0  43281  pell1234qrmulcl  43283  pell14qrdich  43297  pell1qrge1  43298  pellqrex  43307  rmxypairf1o  43339  rmxycomplete  43345  monotoddzzfi  43370  congadd  43394  jm2.19lem3  43419  jm2.19lem4  43420  jm2.25  43427  jm2.26a  43428  jm2.26lem3  43429  expdiophlem1  43449  wepwsolem  43470  lmhmfgsplit  43514  aaitgo  43590  mon1psubm  43627  deg1mhm  43628  succlg  43756  ofoacom  43789  iunrelexp0  44129  isotone2  44476  mnuprdlem4  44702  relpmin  45379  disjrnmpt2  45618  mullimc  46046  mullimcf  46053  climxrre  46178  fprodcncf  46328  stoweidlem17  46445  stoweidlem27  46455  stoweidlem54  46482  fourierdlem42  46577  fourierdlem62  46596  fourierdlem73  46607  fourierdlem76  46610  fourierdlem97  46631  sge0iunmptlemfi  46841  isomenndlem  46958  imarnf1pr  47730  smonoord  47825  fvelsetpreimafv  47847  iccpartiltu  47882  sprsymrelf1lem  47951  prproropf1olem3  47965  paireqne  47971  fmtnoprmfac1  48028  prmdvdsfmtnof1lem2  48048  nprmdvdsfacm1  48087  gricushgr  48393  grimedg  48411  cycl3grtri  48423  gpgedg2iv  48543  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  rngcinvALTV  48752  funcringcsetcALTV2lem9  48774  ringcinvALTV  48786  funcringcsetclem9ALTV  48797  lmodvsmdi  48855  lincsum  48905  lindslinindimp2lem4  48937  nn0sumshdiglemB  49096  1arymaptf1  49118  2arymaptf1  49129  dmrnxp  49312  xpco2  49332  initopropd  49718  termopropd  49719  zeroopropd  49720  oduoppcciso  50041  lanpropd  50090  ranpropd  50091