Theorem ad2antll 725

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 480	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜓)
3	2	adantl 480	1 ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  simprr  769  simprrl  777  simprrr  778  simprr1  1219  simprr2  1220  simprr3  1221  prneimg  4854  fr2nr  5653  wereu2  5672  f1oprg  6877  fvtp1g  7200  funfvima3  7239  isof1oidb  7323  isomin  7336  weniso  7353  elovmpt3rab1  7668  sorpssi  7721  poseq  8146  suppofssd  8190  tfrlem9a  8388  oalimcl  8562  odi  8581  oeeui  8604  ralxpmap  8892  boxriin  8936  domdifsn  9056  domunsncan  9074  enfixsn  9083  disjen  9136  mapen  9143  mapxpen  9145  mapunen  9148  findcard2d  9168  unxpdomlem2  9253  unxpdomlem3  9254  findcard3OLD  9288  isfinite2  9303  marypha1lem  9430  marypha2  9436  supmo  9449  infmo  9492  card2inf  9552  brwdom2  9570  wemapwe  9694  rankonidlem  9825  rankxplim3  9878  djulf1o  9909  djurf1o  9910  infxpenlem  10010  infxpenc2lem1  10016  infxpenc2  10019  fseqenlem1  10021  fseqenlem2  10022  infpwfien  10059  dfac12lem2  10141  infunsdom1  10210  infunsdom  10211  infmap2  10215  fin2i2  10315  fin23lem28  10337  fin23lem32  10341  fin23lem34  10343  fin23lem40  10348  isf32lem2  10351  compssiso  10371  isfin1-3  10383  fin1a2lem10  10406  fin12  10410  hsmexlem4  10426  ac6num  10476  ttukeylem7  10512  axdclem2  10517  iundom2g  10537  fpwwe2lem11  10638  pwfseqlem3  10657  winalim2  10693  winafp  10694  wunex2  10735  grur1  10817  dedekindle  11382  00id  11393  receu  11863  lt2mul2div  12096  peano5uzi  12655  uzwo  12899  qbtwnre  13182  iooshf  13407  modmul1  13893  seqcl2  13990  seqfveq2  13994  seqid2  14018  seqdistr  14023  expcl2lem  14043  mulexpz  14072  expnlbnd2  14201  hashfun  14401  hashfacen  14417  hashfacenOLD  14418  hashf1lem1  14419  hashf1lem1OLD  14420  elss2prb  14452  fstwrdne0  14510  swrdsb0eq  14617  swrdswrd  14659  wrd2ind  14677  swrdccatin1  14679  pfxccatin12  14687  splid  14707  repswrevw  14741  cshwidxmod  14757  cshwidx0  14760  2cshw  14767  cshweqrep  14775  cshw1  14776  wwlktovfo  14913  relexpfld  15000  relexpindlem  15014  01sqrexlem6  15198  absexpz  15256  o1rlimmul  15567  iseralt  15635  summolem2  15666  fsumf1o  15673  fsum0diag2  15733  fsummulc2  15734  cvgcmpce  15768  incexclem  15786  prodmolem2  15883  fprodcl2lem  15898  fprodmul  15908  fprodrev  15925  moddvds  16212  dvdsflip  16264  bitsf1ocnv  16389  sadcaddlem  16402  bezoutlem2  16486  bezoutlem4  16488  dfgcd2  16492  lcmgcdlem  16547  crth  16715  hashgcdlem  16725  phisum  16727  pcqcl  16793  pcid  16810  pcneg  16811  prmpwdvds  16841  pockthg  16843  4sqlem11  16892  ramub2  16951  0ram  16957  prmgaplem7  16994  prmgaplem8  16995  setscom  17117  qusval  17492  initoeu1  17965  termoeu1  17972  setcinv  18044  funcestrcsetclem9  18104  funcsetcestrclem9  18119  fullsetcestrc  18122  1stfcl  18153  2ndfcl  18154  hofpropd  18224  isacs3lem  18499  mgmhmlin  18624  frmdss2  18780  frmdup1  18781  mgm2nsgrplem2  18836  mulgdirlem  19021  mulgass  19027  0nsg  19085  cycsubgcl  19121  ghmmulg  19142  conjghm  19163  qusghm  19169  gsumwrev  19274  symg2bas  19301  symgfixelsi  19344  f1otrspeq  19356  psgnunilem2  19404  psgnunilem3  19405  odf1o2  19482  lsmhash  19614  efgtf  19631  efginvrel2  19636  efgredeu  19661  efgcpbllemb  19664  frgpuplem  19681  frgpup1  19684  ghmcyg  19805  gsumval3lem1  19814  gsumzres  19818  gsumzcl2  19819  gsumzf1o  19821  gsumzaddlem  19830  gsumconst  19843  gsumzmhm  19846  gsumzoppg  19853  gsum2d  19881  subgdmdprd  19945  pgpfac1lem3  19988  gsummgp0  20206  rnghmmul  20340  islmodd  20620  lmodvsmmulgdi  20651  islss3  20714  0lmhm  20795  idlmhm  20796  lmhmeql  20810  pwssplit3  20816  lidldvgen  21093  qsssubdrg  21204  cnsubrg  21205  znf1o  21326  psgnghm  21352  psgndif  21374  cssmre  21465  dsmmsubg  21517  frlmup1  21572  lindfrn  21595  f1lindf  21596  evlslem1  21864  coe1tmmul2  22018  pf1ind  22094  mamufval  22107  mamurid  22164  mvmulfval  22264  mdetralt2  22331  mndifsplit  22358  maducoeval2  22362  madugsum  22365  mat2pmatmul  22453  decpmatmul  22494  pm2mpf1lem  22516  pm2mpf1  22521  monmat2matmon  22546  chpscmat  22564  fvmptnn04if  22571  tgcl  22692  ppttop  22730  epttop  22732  clsval2  22774  opncldf1  22808  mretopd  22816  neindisj  22841  neiptopnei  22856  restcls  22905  restntr  22906  ordtbas  22916  cnpnei  22988  cncls2  22997  tgcmp  23125  cmpcld  23126  uncmp  23127  hauscmplem  23130  1stcfb  23169  2ndcctbss  23179  hauspwdom  23225  reftr  23238  comppfsc  23256  kgentopon  23262  ptpjpre1  23295  ptcnplem  23345  txcn  23350  txdis1cn  23359  txhaus  23371  xkopt  23379  imasnopn  23414  imasncld  23415  imasncls  23416  hmeoimaf1o  23494  cmphaushmeo  23524  txhmeo  23527  trfbas2  23567  fbasfip  23592  fbasrn  23608  fmss  23670  elfm2  23672  hauspwpwf1  23711  flfcnp  23728  fclscf  23749  flimfnfcls  23752  fcfval  23757  alexsubALTlem2  23772  alexsubALTlem3  23773  alexsubALTlem4  23774  ptcmplem3  23778  ptcmplem4  23779  cnextfval  23786  cnextcn  23791  tmdgsum2  23820  ustex2sym  23941  neipcfilu  24021  imasdsf1olem  24099  metss2lem  24240  stdbdxmet  24244  stdbdmopn  24247  metrest  24253  metcnp  24270  restmetu  24299  tngngp  24391  icccmplem1  24558  icccvx  24695  evth  24705  lebnumlem1  24707  pi1blem  24786  isncvsngp  24897  equivcau  25048  bcthlem5  25076  cmslssbn  25120  ivthlem3  25202  ovolicc2lem3  25268  ovolicc2lem4  25269  dyaddisj  25345  dyadmbllem  25348  ismbfd  25388  itg2seq  25492  itgss  25561  limciun  25643  dvcobr  25697  dvcobrOLD  25698  dvmptfsum  25727  c1liplem1  25748  c1lip1  25749  lhop  25768  dvcvx  25772  tdeglem4  25812  plyco0  25941  elply2  25945  plypf1  25961  dgreq0  26015  elqaalem2  26069  aalioulem6  26086  aaliou  26087  aaliou2b  26090  ulmss  26145  ulmcn  26147  pserulm  26170  lgamgulmlem5  26773  basellem4  26824  fsumdvdsdiaglem  26923  dvdsmulf1o  26934  chtublem  26950  fsumvma2  26953  logfaclbnd  26961  dchrelbasd  26978  lgsqrlem2  27086  gausslemma2dlem1a  27104  lgseisenlem2  27115  lgsquadlem1  27119  lgsquadlem2  27120  lgsquadlem3  27121  rplogsumlem2  27224  rpvmasumlem  27226  dchrmusum2  27233  dchrvmasumlem1  27234  dchrvmasum2lem  27235  rpvmasum2  27251  dchrisum0lem1  27255  logsqvma  27281  selberg4  27300  pntibndlem3  27331  pntlem3  27348  ostthlem1  27366  ostthlem2  27367  sltres  27401  nogt01o  27435  oldbdayim  27620  addsproplem2  27692  negsproplem2  27742  mulsval  27804  idmot  28055  brcgr  28425  brbtwn2  28430  axsegconlem8  28449  axpaschlem  28465  axeuclid  28488  axcontlem2  28490  axcontlem7  28495  eengtrkg  28511  upgrex  28619  subgrprop3  28800  subupgr  28811  nbgr0vtxlem  28879  nb3grprlem1  28904  cusgredg  28948  cusgrres  28972  usgredgsscusgredg  28983  finsumvtxdg2ssteplem4  29072  finsumvtxdg2sstep  29073  wlkl1loop  29162  wlkp1lem4  29200  wwlksnred  29413  wwlksnext  29414  wwlksnextwrd  29418  wpthswwlks2on  29482  clwwlknp  29557  clwwlkel  29566  wwlksext2clwwlk  29577  clwwlknonwwlknonb  29626  3wlkond  29691  1conngr  29714  eucrctshift  29763  fusgr2wsp2nb  29854  numclwwlk1lem2foa  29874  numclwwlk1lem2f1  29877  numclwlk1lem1  29889  numclwlk1lem2  29890  grpoidinvlem1  30024  grporcan  30038  ipblnfi  30375  hvmulcan2  30593  shscli  30837  spansneleq  31090  pjspansn  31097  3oalem2  31183  eigposi  31356  cnlnadjlem2  31588  stlesi  31761  mdslmd1lem1  31845  mdslmd1lem2  31846  cdj1i  31953  disjxpin  32086  nn0xmulclb  32251  xreceu  32355  txomap  33112  pstmxmet  33175  qqhghm  33266  qqhrhm  33267  measinblem  33516  cntmeas  33522  ballotlemsf1o  33810  bnj945  34082  bnj1110  34291  f1resveqaeq  34386  cvmopnlem  34567  cvmfolem  34568  cvmliftmolem2  34571  cvmlift2lem10  34601  satf00  34663  satffunlem2lem1  34693  satefvfmla0  34707  mrsubvrs  34811  wzel  35100  btwnconn1lem8  35370  btwnconn1lem9  35371  btwnconn1lem10  35372  btwnconn1lem11  35373  btwnconn1lem12  35374  finminlem  35506  nn0prpwlem  35510  fnessref  35545  refssfne  35546  fnemeet2  35555  consym1  35608  bj-finsumval0  36469  topdifinffinlem  36531  relowlssretop  36547  rdgeqoa  36554  fvineqsneu  36595  pibt2  36601  matunitlindflem1  36787  poimirlem28  36819  mblfinlem1  36828  mblfinlem3  36830  mblfinlem4  36831  ovoliunnfl  36833  mbfresfi  36837  mbfposadd  36838  itg2addnclem2  36843  itg2addnc  36845  ftc1anc  36872  frinfm  36906  fdc  36916  blssp  36927  sstotbnd  36946  isbnd2  36954  ssbnd  36959  prdstotbnd  36965  prdsbnd2  36966  ismtyres  36979  heibor1lem  36980  rrnequiv  37006  rngoisocnv  37152  crngohomfo  37177  pridlc3  37244  membpartlem19  37984  prter3  38055  ax12eq  38114  ax12el  38115  cvratlem  38595  islvol2aN  38766  4atlem4b  38774  4atlem4c  38775  4atlem4d  38776  isline2  38948  isline3  38950  pclfinclN  39124  linepsubclN  39125  pexmidlem4N  39147  diaglbN  40229  dvhvaddcl  40269  dvhvaddcomN  40270  dvhvscacl  40277  djavalN  40309  dibglbN  40340  dihatexv  40512  djhval  40572  mapdrvallem2  40819  metakunt15  41305  evlselvlem  41460  evlselv  41461  mhpind  41468  prjsprellsp  41655  elrfi  41734  nacsfix  41752  eldioph2  41802  lzenom  41810  rexrabdioph  41834  irrapxlem3  41864  pellexlem5  41873  pellex  41875  pell1234qrne0  41893  pell1234qrmulcl  41895  pell14qrdich  41909  pell1qrge1  41910  pellqrex  41919  rmxypairf1o  41952  rmxycomplete  41958  monotoddzzfi  41983  congadd  42007  jm2.19lem3  42032  jm2.19lem4  42033  jm2.25  42040  jm2.26a  42041  jm2.26lem3  42042  expdiophlem1  42062  wepwsolem  42086  lmhmfgsplit  42130  aaitgo  42206  mon1psubm  42250  deg1mhm  42251  succlg  42380  ofoacom  42413  iunrelexp0  42755  isotone2  43102  mnuprdlem4  43336  disjrnmpt2  44185  mullimc  44630  mullimcf  44637  climxrre  44764  fprodcncf  44914  stoweidlem17  45031  stoweidlem27  45041  stoweidlem54  45068  fourierdlem42  45163  fourierdlem62  45182  fourierdlem73  45193  fourierdlem76  45196  fourierdlem97  45217  sge0iunmptlemfi  45427  isomenndlem  45544  imarnf1pr  46288  smonoord  46337  fvelsetpreimafv  46353  iccpartiltu  46388  sprsymrelf1lem  46457  prproropf1olem3  46471  paireqne  46477  fmtnoprmfac1  46531  prmdvdsfmtnof1lem2  46551  isomushgr  46792  isomuspgrlem2c  46796  rngcinv  46967  rngcinvALTV  46979  ringcinv  47018  funcringcsetcALTV2lem9  47030  ringcinvALTV  47042  funcringcsetclem9ALTV  47053  mndpsuppss  47135  lmodvsmdi  47146  lincsum  47197  lindslinindimp2lem4  47229  nn0sumshdiglemB  47393  1arymaptf1  47415  2arymaptf1  47426