Theorem ad2antll 728

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  772  simprrl  780  simprrr  781  simprr1  1221  simprr2  1222  simprr3  1223  prneimg  4879  prproe  4929  fr2nr  5677  wereu2  5697  f1oprg  6907  fvtp1g  7235  funfvima3  7273  isof1oidb  7360  isomin  7373  weniso  7390  elovmpt3rab1  7710  sorpssi  7764  poseq  8199  suppofssd  8244  tfrlem9a  8442  oalimcl  8616  odi  8635  oeeui  8658  ralxpmap  8954  boxriin  8998  domdifsn  9120  domunsncan  9138  enfixsn  9147  disjen  9200  mapen  9207  mapxpen  9209  mapunen  9212  findcard2d  9232  unxpdomlem2  9314  unxpdomlem3  9315  findcard3OLD  9347  isfinite2  9362  marypha1lem  9502  marypha2  9508  supmo  9521  infmo  9564  card2inf  9624  brwdom2  9642  wemapwe  9766  rankonidlem  9897  rankxplim3  9950  djulf1o  9981  djurf1o  9982  infxpenlem  10082  infxpenc2lem1  10088  infxpenc2  10091  fseqenlem1  10093  fseqenlem2  10094  infpwfien  10131  dfac12lem2  10214  infunsdom1  10281  infunsdom  10282  infmap2  10286  fin2i2  10387  fin23lem28  10409  fin23lem32  10413  fin23lem34  10415  fin23lem40  10420  isf32lem2  10423  compssiso  10443  isfin1-3  10455  fin1a2lem10  10478  fin12  10482  hsmexlem4  10498  ac6num  10548  ttukeylem7  10584  axdclem2  10589  iundom2g  10609  fpwwe2lem11  10710  pwfseqlem3  10729  winalim2  10765  winafp  10766  wunex2  10807  grur1  10889  dedekindle  11454  00id  11465  receu  11935  lt2mul2div  12173  peano5uzi  12732  uzwo  12976  qbtwnre  13261  iooshf  13486  modmul1  13975  seqcl2  14071  seqfveq2  14075  seqid2  14099  seqdistr  14104  expcl2lem  14124  mulexpz  14153  expnlbnd2  14283  hashfun  14486  hashfacen  14503  hashf1lem1  14504  elss2prb  14537  fstwrdne0  14604  swrdsb0eq  14711  swrdswrd  14753  wrd2ind  14771  swrdccatin1  14773  pfxccatin12  14781  splid  14801  repswrevw  14835  cshwidxmod  14851  cshwidx0  14854  2cshw  14861  cshweqrep  14869  cshw1  14870  wwlktovfo  15007  relexpfld  15098  relexpindlem  15112  01sqrexlem6  15296  absexpz  15354  o1rlimmul  15665  iseralt  15733  summolem2  15764  fsumf1o  15771  fsum0diag2  15831  fsummulc2  15832  cvgcmpce  15866  incexclem  15884  prodmolem2  15983  fprodcl2lem  15998  fprodmul  16008  fprodrev  16025  moddvds  16313  dvdsflip  16365  bitsf1ocnv  16490  sadcaddlem  16503  bezoutlem2  16587  bezoutlem4  16589  dfgcd2  16593  lcmgcdlem  16653  crth  16825  hashgcdlem  16835  phisum  16837  pcqcl  16903  pcid  16920  pcneg  16921  prmpwdvds  16951  pockthg  16953  4sqlem11  17002  ramub2  17061  0ram  17067  prmgaplem7  17104  prmgaplem8  17105  setscom  17227  qusval  17602  initoeu1  18078  termoeu1  18085  setcinv  18157  funcestrcsetclem9  18217  funcsetcestrclem9  18232  fullsetcestrc  18235  1stfcl  18266  2ndfcl  18267  hofpropd  18337  isacs3lem  18612  mgmhmlin  18737  frmdss2  18898  frmdup1  18899  mgm2nsgrplem2  18954  mulgdirlem  19145  mulgass  19151  0nsg  19209  cycsubgcl  19246  ghmmulg  19268  conjghm  19289  qusghm  19295  gsumwrev  19409  symg2bas  19434  symgfixelsi  19477  f1otrspeq  19489  psgnunilem2  19537  psgnunilem3  19538  odf1o2  19615  lsmhash  19747  efgtf  19764  efginvrel2  19769  efgredeu  19794  efgcpbllemb  19797  frgpuplem  19814  frgpup1  19817  ghmcyg  19938  gsumval3lem1  19947  gsumzres  19951  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumconst  19976  gsumzmhm  19979  gsumzoppg  19986  gsum2d  20014  subgdmdprd  20078  pgpfac1lem3  20121  gsummgp0  20341  rnghmmul  20475  rngcinv  20659  ringcinv  20693  islmodd  20886  lmodvsmmulgdi  20917  islss3  20980  0lmhm  21062  idlmhm  21063  lmhmeql  21077  pwssplit3  21083  lidldvgen  21367  qsssubdrg  21467  cnsubrg  21468  znf1o  21593  psgnghm  21621  psgndif  21643  cssmre  21734  dsmmsubg  21786  frlmup1  21841  lindfrn  21864  f1lindf  21865  evlslem1  22129  psdmul  22193  coe1tmmul2  22300  pf1ind  22380  mamufval  22417  mamurid  22469  mvmulfval  22569  mdetralt2  22636  mndifsplit  22663  maducoeval2  22667  madugsum  22670  mat2pmatmul  22758  decpmatmul  22799  pm2mpf1lem  22821  pm2mpf1  22826  monmat2matmon  22851  chpscmat  22869  fvmptnn04if  22876  tgcl  22997  ppttop  23035  epttop  23037  clsval2  23079  opncldf1  23113  mretopd  23121  neindisj  23146  neiptopnei  23161  restcls  23210  restntr  23211  ordtbas  23221  cnpnei  23293  cncls2  23302  tgcmp  23430  cmpcld  23431  uncmp  23432  hauscmplem  23435  1stcfb  23474  2ndcctbss  23484  hauspwdom  23530  reftr  23543  comppfsc  23561  kgentopon  23567  ptpjpre1  23600  ptcnplem  23650  txcn  23655  txdis1cn  23664  txhaus  23676  xkopt  23684  imasnopn  23719  imasncld  23720  imasncls  23721  hmeoimaf1o  23799  cmphaushmeo  23829  txhmeo  23832  trfbas2  23872  fbasfip  23897  fbasrn  23913  fmss  23975  elfm2  23977  hauspwpwf1  24016  flfcnp  24033  fclscf  24054  flimfnfcls  24057  fcfval  24062  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem3  24083  ptcmplem4  24084  cnextfval  24091  cnextcn  24096  tmdgsum2  24125  ustex2sym  24246  neipcfilu  24326  imasdsf1olem  24404  metss2lem  24545  stdbdxmet  24549  stdbdmopn  24552  metrest  24558  metcnp  24575  restmetu  24604  tngngp  24696  icccmplem1  24863  icccvx  25000  evth  25010  lebnumlem1  25012  pi1blem  25091  isncvsngp  25202  equivcau  25353  bcthlem5  25381  cmslssbn  25425  ivthlem3  25507  ovolicc2lem3  25573  ovolicc2lem4  25574  dyaddisj  25650  dyadmbllem  25653  ismbfd  25693  itg2seq  25797  itgss  25867  limciun  25949  dvcobr  26003  dvcobrOLD  26004  dvmptfsum  26033  c1liplem1  26055  c1lip1  26056  lhop  26075  dvcvx  26079  tdeglem4  26119  plyco0  26251  elply2  26255  plypf1  26271  dgreq0  26325  elqaalem2  26380  aalioulem6  26397  aaliou  26398  aaliou2b  26401  ulmss  26458  ulmcn  26460  pserulm  26483  lgamgulmlem5  27094  basellem4  27145  fsumdvdsdiaglem  27244  mpodvdsmulf1o  27255  dvdsmulf1o  27257  chtublem  27273  fsumvma2  27276  logfaclbnd  27284  dchrelbasd  27301  lgsqrlem2  27409  gausslemma2dlem1a  27427  lgseisenlem2  27438  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  rplogsumlem2  27547  rpvmasumlem  27549  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  rpvmasum2  27574  dchrisum0lem1  27578  logsqvma  27604  selberg4  27623  pntibndlem3  27654  pntlem3  27671  ostthlem1  27689  ostthlem2  27690  sltres  27725  nogt01o  27759  oldbdayim  27945  addsproplem2  28021  negsproplem2  28079  mulsval  28153  om2noseqrdg  28328  noseqrdgfn  28330  zmulscld  28401  recut  28446  idmot  28563  brcgr  28933  brbtwn2  28938  axsegconlem8  28957  axpaschlem  28973  axeuclid  28996  axcontlem2  28998  axcontlem7  29003  eengtrkg  29019  upgrex  29127  subgrprop3  29311  subupgr  29322  nbgr0edglem  29391  nb3grprlem1  29415  cusgredg  29459  cusgrres  29484  usgredgsscusgredg  29495  finsumvtxdg2ssteplem4  29584  finsumvtxdg2sstep  29585  wlkl1loop  29674  wlkp1lem4  29712  wwlksnred  29925  wwlksnext  29926  wwlksnextwrd  29930  wpthswwlks2on  29994  clwwlknp  30069  clwwlkel  30078  wwlksext2clwwlk  30089  clwwlknonwwlknonb  30138  3wlkond  30203  1conngr  30226  eucrctshift  30275  fusgr2wsp2nb  30366  numclwwlk1lem2foa  30386  numclwwlk1lem2f1  30389  numclwlk1lem1  30401  numclwlk1lem2  30402  grpoidinvlem1  30536  grporcan  30550  ipblnfi  30887  hvmulcan2  31105  shscli  31349  spansneleq  31602  pjspansn  31609  3oalem2  31695  eigposi  31868  cnlnadjlem2  32100  stlesi  32273  mdslmd1lem1  32357  mdslmd1lem2  32358  cdj1i  32465  disjxpin  32610  nn0xmulclb  32778  xreceu  32886  txomap  33780  pstmxmet  33843  qqhghm  33934  qqhrhm  33935  measinblem  34184  cntmeas  34190  ballotlemsf1o  34478  bnj945  34749  bnj1110  34958  f1resveqaeq  35061  cvmopnlem  35246  cvmfolem  35247  cvmliftmolem2  35250  cvmlift2lem10  35280  satf00  35342  satffunlem2lem1  35372  satefvfmla0  35386  mrsubvrs  35490  wzel  35788  btwnconn1lem8  36058  btwnconn1lem9  36059  btwnconn1lem10  36060  btwnconn1lem11  36061  btwnconn1lem12  36062  finminlem  36284  nn0prpwlem  36288  fnessref  36323  refssfne  36324  fnemeet2  36333  consym1  36386  bj-finsumval0  37251  topdifinffinlem  37313  relowlssretop  37329  rdgeqoa  37336  fvineqsneu  37377  pibt2  37383  matunitlindflem1  37576  poimirlem28  37608  mblfinlem1  37617  mblfinlem3  37619  mblfinlem4  37620  ovoliunnfl  37622  mbfresfi  37626  mbfposadd  37627  itg2addnclem2  37632  itg2addnc  37634  ftc1anc  37661  frinfm  37695  fdc  37705  blssp  37716  sstotbnd  37735  isbnd2  37743  ssbnd  37748  prdstotbnd  37754  prdsbnd2  37755  ismtyres  37768  heibor1lem  37769  rrnequiv  37795  rngoisocnv  37941  crngohomfo  37966  pridlc3  38033  membpartlem19  38767  prter3  38838  ax12eq  38897  ax12el  38898  cvratlem  39378  islvol2aN  39549  4atlem4b  39557  4atlem4c  39558  4atlem4d  39559  isline2  39731  isline3  39733  pclfinclN  39907  linepsubclN  39908  pexmidlem4N  39930  diaglbN  41012  dvhvaddcl  41052  dvhvaddcomN  41053  dvhvscacl  41060  djavalN  41092  dibglbN  41123  dihatexv  41295  djhval  41355  mapdrvallem2  41602  metakunt15  42176  evlselvlem  42541  evlselv  42542  mhpind  42549  prjsprellsp  42566  elrfi  42650  nacsfix  42668  eldioph2  42718  lzenom  42726  rexrabdioph  42750  irrapxlem3  42780  pellexlem5  42789  pellex  42791  pell1234qrne0  42809  pell1234qrmulcl  42811  pell14qrdich  42825  pell1qrge1  42826  pellqrex  42835  rmxypairf1o  42868  rmxycomplete  42874  monotoddzzfi  42899  congadd  42923  jm2.19lem3  42948  jm2.19lem4  42949  jm2.25  42956  jm2.26a  42957  jm2.26lem3  42958  expdiophlem1  42978  wepwsolem  42999  lmhmfgsplit  43043  aaitgo  43119  mon1psubm  43160  deg1mhm  43161  succlg  43290  ofoacom  43323  iunrelexp0  43664  isotone2  44011  mnuprdlem4  44244  disjrnmpt2  45095  mullimc  45537  mullimcf  45544  climxrre  45671  fprodcncf  45821  stoweidlem17  45938  stoweidlem27  45948  stoweidlem54  45975  fourierdlem42  46070  fourierdlem62  46089  fourierdlem73  46100  fourierdlem76  46103  fourierdlem97  46124  sge0iunmptlemfi  46334  isomenndlem  46451  imarnf1pr  47197  smonoord  47245  fvelsetpreimafv  47261  iccpartiltu  47296  sprsymrelf1lem  47365  prproropf1olem3  47379  paireqne  47385  fmtnoprmfac1  47439  prmdvdsfmtnof1lem2  47459  uspgrimprop  47757  gricushgr  47770  grimedg  47787  rngcinvALTV  47999  funcringcsetcALTV2lem9  48021  ringcinvALTV  48033  funcringcsetclem9ALTV  48044  mndpsuppss  48096  lmodvsmdi  48107  lincsum  48158  lindslinindimp2lem4  48190  nn0sumshdiglemB  48354  1arymaptf1  48376  2arymaptf1  48387