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  4812  prproe  4863  fr2nr  5609  wereu2  5629  f1oprg  6828  fvtp1g  7154  funfvima3  7192  isof1oidb  7280  isomin  7293  weniso  7310  elovmpt3rab1  7628  sorpssi  7684  resf1extb  7886  poseq  8110  suppofssd  8155  tfrlem9a  8327  oalimcl  8497  odi  8516  oeeui  8540  ralxpmap  8846  boxriin  8890  domdifsn  9000  domunsncan  9017  enfixsn  9026  disjen  9074  mapen  9081  mapxpen  9083  mapunen  9086  findcard2d  9103  unxpdomlem2  9169  unxpdomlem3  9170  isfinite2  9210  marypha1lem  9348  marypha2  9354  supmo  9367  infmo  9412  card2inf  9472  brwdom2  9490  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  11309  00id  11320  receu  11794  lt2mul2div  12032  peano5uzi  12593  uzwo  12836  qbtwnre  13126  iooshf  13354  modmul1  13859  seqcl2  13955  seqfveq2  13959  seqid2  13983  seqdistr  13988  expcl2lem  14008  mulexpz  14037  expnlbnd2  14169  hashfun  14372  hashfacen  14389  hashf1lem1  14390  elss2prb  14423  fstwrdne0  14491  swrdsb0eq  14599  swrdswrd  14640  wrd2ind  14658  swrdccatin1  14660  pfxccatin12  14668  splid  14688  repswrevw  14722  cshwidxmod  14738  cshwidx0  14741  2cshw  14748  cshweqrep  14756  cshw1  14757  wwlktovfo  14893  relexpfld  14984  relexpindlem  14998  01sqrexlem6  15182  absexpz  15240  o1rlimmul  15554  iseralt  15620  summolem2  15651  fsumf1o  15658  fsum0diag2  15718  fsummulc2  15719  cvgcmpce  15753  incexclem  15771  prodmolem2  15870  fprodcl2lem  15885  fprodmul  15895  fprodrev  15912  moddvds  16202  dvdsflip  16256  bitsf1ocnv  16383  sadcaddlem  16396  bezoutlem2  16479  bezoutlem4  16481  dfgcd2  16485  lcmgcdlem  16545  crth  16717  hashgcdlem  16727  phisum  16730  pcqcl  16796  pcid  16813  pcneg  16814  prmpwdvds  16844  pockthg  16846  4sqlem11  16895  ramub2  16954  0ram  16960  prmgaplem7  16997  prmgaplem8  16998  setscom  17119  qusval  17475  initoeu1  17947  termoeu1  17954  setcinv  18026  funcestrcsetclem9  18083  funcsetcestrclem9  18098  fullsetcestrc  18101  1stfcl  18132  2ndfcl  18133  hofpropd  18202  isacs3lem  18477  mgmhmlin  18636  mndpsuppss  18702  frmdss2  18800  frmdup1  18801  mgm2nsgrplem2  18859  mulgdirlem  19050  mulgass  19056  0nsg  19113  cycsubgcl  19150  ghmmulg  19172  conjghm  19193  qusghm  19199  gsumwrev  19310  symg2bas  19337  symgfixelsi  19379  f1otrspeq  19391  psgnunilem2  19439  psgnunilem3  19440  odf1o2  19517  lsmhash  19649  efgtf  19666  efginvrel2  19671  efgredeu  19696  efgcpbllemb  19699  frgpuplem  19716  frgpup1  19719  ghmcyg  19840  gsumval3lem1  19849  gsumzres  19853  gsumzcl2  19854  gsumzf1o  19856  gsumzaddlem  19865  gsumconst  19878  gsumzmhm  19881  gsumzoppg  19888  gsum2d  19916  subgdmdprd  19980  pgpfac1lem3  20023  gsummgp0  20268  rnghmmul  20400  rngcinv  20585  ringcinv  20619  islmodd  20832  lmodvsmmulgdi  20863  islss3  20925  0lmhm  21007  idlmhm  21008  lmhmeql  21022  pwssplit3  21028  lidldvgen  21304  qsssubdrg  21396  cnsubrg  21397  znf1o  21521  psgnghm  21550  psgndif  21572  cssmre  21663  dsmmsubg  21713  frlmup1  21768  lindfrn  21791  f1lindf  21792  evlslem1  22052  psdmul  22124  coe1tmmul2  22233  pf1ind  22314  mamufval  22351  mamurid  22401  mvmulfval  22501  mdetralt2  22568  mndifsplit  22595  maducoeval2  22599  madugsum  22602  mat2pmatmul  22690  decpmatmul  22731  pm2mpf1lem  22753  pm2mpf1  22758  monmat2matmon  22783  chpscmat  22801  fvmptnn04if  22808  tgcl  22928  ppttop  22966  epttop  22968  clsval2  23009  opncldf1  23043  mretopd  23051  neindisj  23076  neiptopnei  23091  restcls  23140  restntr  23141  ordtbas  23151  cnpnei  23223  cncls2  23232  tgcmp  23360  cmpcld  23361  uncmp  23362  hauscmplem  23365  1stcfb  23404  2ndcctbss  23414  hauspwdom  23460  reftr  23473  comppfsc  23491  kgentopon  23497  ptpjpre1  23530  ptcnplem  23580  txcn  23585  txdis1cn  23594  txhaus  23606  xkopt  23614  imasnopn  23649  imasncld  23650  imasncls  23651  hmeoimaf1o  23729  cmphaushmeo  23759  txhmeo  23762  trfbas2  23802  fbasfip  23827  fbasrn  23843  fmss  23905  elfm2  23907  hauspwpwf1  23946  flfcnp  23963  fclscf  23984  flimfnfcls  23987  fcfval  23992  alexsubALTlem2  24007  alexsubALTlem3  24008  alexsubALTlem4  24009  ptcmplem3  24013  ptcmplem4  24014  cnextfval  24021  cnextcn  24026  tmdgsum2  24055  ustex2sym  24176  neipcfilu  24254  imasdsf1olem  24332  metss2lem  24470  stdbdxmet  24474  stdbdmopn  24477  metrest  24483  metcnp  24500  restmetu  24529  tngngp  24613  icccmplem1  24782  icccvx  24919  evth  24929  lebnumlem1  24931  pi1blem  25010  isncvsngp  25120  equivcau  25271  bcthlem5  25299  cmslssbn  25343  ivthlem3  25425  ovolicc2lem3  25491  ovolicc2lem4  25492  dyaddisj  25568  dyadmbllem  25571  ismbfd  25611  itg2seq  25714  itgss  25784  limciun  25866  dvcobr  25920  dvcobrOLD  25921  dvmptfsum  25950  c1liplem1  25972  c1lip1  25973  lhop  25992  dvcvx  25996  tdeglem4  26036  plyco0  26168  elply2  26172  plypf1  26188  dgreq0  26242  elqaalem2  26299  aalioulem6  26316  aaliou  26317  aaliou2b  26320  ulmss  26377  ulmcn  26379  pserulm  26402  lgamgulmlem5  27014  basellem4  27065  fsumdvdsdiaglem  27164  mpodvdsmulf1o  27175  dvdsmulf1o  27177  chtublem  27193  fsumvma2  27196  logfaclbnd  27204  dchrelbasd  27221  lgsqrlem2  27329  gausslemma2dlem1a  27347  lgseisenlem2  27358  lgsquadlem1  27362  lgsquadlem2  27363  lgsquadlem3  27364  rplogsumlem2  27467  rpvmasumlem  27469  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2lem  27478  rpvmasum2  27494  dchrisum0lem1  27498  logsqvma  27524  selberg4  27543  pntibndlem3  27574  pntlem3  27591  ostthlem1  27609  ostthlem2  27610  ltsres  27645  nogt01o  27679  oldbdayim  27900  addsproplem2  27981  negsproplem2  28040  mulsval  28120  om2noseqrdg  28315  noseqrdgfn  28317  zmulscld  28408  recut  28505  idmot  28625  brcgr  28989  brbtwn2  28994  axsegconlem8  29013  axpaschlem  29029  axeuclid  29052  axcontlem2  29054  axcontlem7  29059  eengtrkg  29075  upgrex  29181  subgrprop3  29365  subupgr  29376  nbgr0edglem  29445  nb3grprlem1  29469  cusgredg  29513  cusgrres  29538  usgredgsscusgredg  29549  finsumvtxdg2ssteplem4  29638  finsumvtxdg2sstep  29639  wlkl1loop  29727  wlkp1lem4  29764  wwlksnred  29981  wwlksnext  29982  wwlksnextwrd  29986  wpthswwlks2on  30053  clwwlknp  30128  clwwlkel  30137  wwlksext2clwwlk  30148  clwwlknonwwlknonb  30197  3wlkond  30262  1conngr  30285  eucrctshift  30334  fusgr2wsp2nb  30425  numclwwlk1lem2foa  30445  numclwwlk1lem2f1  30448  numclwlk1lem1  30460  numclwlk1lem2  30461  grpoidinvlem1  30596  grporcan  30610  ipblnfi  30947  hvmulcan2  31165  shscli  31409  spansneleq  31662  pjspansn  31669  3oalem2  31755  eigposi  31928  cnlnadjlem2  32160  stlesi  32333  mdslmd1lem1  32417  mdslmd1lem2  32418  cdj1i  32525  disjxpin  32679  nn0xmulclb  32866  xreceu  33018  txomap  34016  pstmxmet  34079  qqhghm  34170  qqhrhm  34171  measinblem  34402  cntmeas  34408  ballotlemsf1o  34696  bnj945  34954  bnj1110  35162  f1resveqaeq  35266  rankfilimbi  35282  cvmopnlem  35498  cvmfolem  35499  cvmliftmolem2  35502  cvmlift2lem10  35532  satf00  35594  satffunlem2lem1  35624  satefvfmla0  35638  mrsubvrs  35742  wzel  36042  btwnconn1lem8  36314  btwnconn1lem9  36315  btwnconn1lem10  36316  btwnconn1lem11  36317  btwnconn1lem12  36318  finminlem  36538  nn0prpwlem  36542  fnessref  36577  refssfne  36578  fnemeet2  36587  consym1  36640  bj-finsumval0  37544  topdifinffinlem  37606  relowlssretop  37622  rdgeqoa  37629  fvineqsneu  37670  pibt2  37676  matunitlindflem1  37871  poimirlem28  37903  mblfinlem1  37912  mblfinlem3  37914  mblfinlem4  37915  ovoliunnfl  37917  mbfresfi  37921  mbfposadd  37922  itg2addnclem2  37927  itg2addnc  37929  ftc1anc  37956  frinfm  37990  fdc  38000  blssp  38011  sstotbnd  38030  isbnd2  38038  ssbnd  38043  prdstotbnd  38049  prdsbnd2  38050  ismtyres  38063  heibor1lem  38064  rrnequiv  38090  rngoisocnv  38236  crngohomfo  38261  pridlc3  38328  membpartlem19  39169  prter3  39262  ax12eq  39321  ax12el  39322  cvratlem  39801  islvol2aN  39972  4atlem4b  39980  4atlem4c  39981  4atlem4d  39982  isline2  40154  isline3  40156  pclfinclN  40330  linepsubclN  40331  pexmidlem4N  40353  diaglbN  41435  dvhvaddcl  41475  dvhvaddcomN  41476  dvhvscacl  41483  djavalN  41515  dibglbN  41546  dihatexv  41718  djhval  41778  mapdrvallem2  42025  evlselvlem  42948  evlselv  42949  mhpind  42956  prjsprellsp  42973  elrfi  43055  nacsfix  43073  eldioph2  43123  lzenom  43131  rexrabdioph  43155  irrapxlem3  43185  pellexlem5  43194  pellex  43196  pell1234qrne0  43214  pell1234qrmulcl  43216  pell14qrdich  43230  pell1qrge1  43231  pellqrex  43240  rmxypairf1o  43272  rmxycomplete  43278  monotoddzzfi  43303  congadd  43327  jm2.19lem3  43352  jm2.19lem4  43353  jm2.25  43360  jm2.26a  43361  jm2.26lem3  43362  expdiophlem1  43382  wepwsolem  43403  lmhmfgsplit  43447  aaitgo  43523  mon1psubm  43560  deg1mhm  43561  succlg  43689  ofoacom  43722  iunrelexp0  44062  isotone2  44409  mnuprdlem4  44635  relpmin  45312  disjrnmpt2  45551  mullimc  45980  mullimcf  45987  climxrre  46112  fprodcncf  46262  stoweidlem17  46379  stoweidlem27  46389  stoweidlem54  46416  fourierdlem42  46511  fourierdlem62  46530  fourierdlem73  46541  fourierdlem76  46544  fourierdlem97  46565  sge0iunmptlemfi  46775  isomenndlem  46892  imarnf1pr  47646  smonoord  47735  fvelsetpreimafv  47751  iccpartiltu  47786  sprsymrelf1lem  47855  prproropf1olem3  47869  paireqne  47875  fmtnoprmfac1  47929  prmdvdsfmtnof1lem2  47949  gricushgr  48281  grimedg  48299  cycl3grtri  48311  gpgedg2iv  48431  pgnbgreunbgrlem2lem1  48478  pgnbgreunbgrlem2lem2  48479  rngcinvALTV  48640  funcringcsetcALTV2lem9  48662  ringcinvALTV  48674  funcringcsetclem9ALTV  48685  lmodvsmdi  48743  lincsum  48793  lindslinindimp2lem4  48825  nn0sumshdiglemB  48984  1arymaptf1  49006  2arymaptf1  49017  dmrnxp  49200  xpco2  49220  initopropd  49606  termopropd  49607  zeroopropd  49608  oduoppcciso  49929  lanpropd  49978  ranpropd  49979