Theorem ad2antll 729

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  1220  simprr2  1221  simprr3  1222  prneimg  4858  prproe  4909  fr2nr  5665  wereu2  5685  f1oprg  6893  fvtp1g  7217  funfvima3  7255  isof1oidb  7343  isomin  7356  weniso  7373  elovmpt3rab1  7692  sorpssi  7747  poseq  8181  suppofssd  8226  tfrlem9a  8424  oalimcl  8596  odi  8615  oeeui  8638  ralxpmap  8934  boxriin  8978  domdifsn  9092  domunsncan  9110  enfixsn  9119  disjen  9172  mapen  9179  mapxpen  9181  mapunen  9184  findcard2d  9204  unxpdomlem2  9284  unxpdomlem3  9285  findcard3OLD  9316  isfinite2  9331  marypha1lem  9470  marypha2  9476  supmo  9489  infmo  9532  card2inf  9592  brwdom2  9610  wemapwe  9734  rankonidlem  9865  rankxplim3  9918  djulf1o  9949  djurf1o  9950  infxpenlem  10050  infxpenc2lem1  10056  infxpenc2  10059  fseqenlem1  10061  fseqenlem2  10062  infpwfien  10099  dfac12lem2  10182  infunsdom1  10249  infunsdom  10250  infmap2  10254  fin2i2  10355  fin23lem28  10377  fin23lem32  10381  fin23lem34  10383  fin23lem40  10388  isf32lem2  10391  compssiso  10411  isfin1-3  10423  fin1a2lem10  10446  fin12  10450  hsmexlem4  10466  ac6num  10516  ttukeylem7  10552  axdclem2  10557  iundom2g  10577  fpwwe2lem11  10678  pwfseqlem3  10697  winalim2  10733  winafp  10734  wunex2  10775  grur1  10857  dedekindle  11422  00id  11433  receu  11905  lt2mul2div  12143  peano5uzi  12704  uzwo  12950  qbtwnre  13237  iooshf  13462  modmul1  13961  seqcl2  14057  seqfveq2  14061  seqid2  14085  seqdistr  14090  expcl2lem  14110  mulexpz  14139  expnlbnd2  14269  hashfun  14472  hashfacen  14489  hashf1lem1  14490  elss2prb  14523  fstwrdne0  14590  swrdsb0eq  14697  swrdswrd  14739  wrd2ind  14757  swrdccatin1  14759  pfxccatin12  14767  splid  14787  repswrevw  14821  cshwidxmod  14837  cshwidx0  14840  2cshw  14847  cshweqrep  14855  cshw1  14856  wwlktovfo  14993  relexpfld  15084  relexpindlem  15098  01sqrexlem6  15282  absexpz  15340  o1rlimmul  15651  iseralt  15717  summolem2  15748  fsumf1o  15755  fsum0diag2  15815  fsummulc2  15816  cvgcmpce  15850  incexclem  15868  prodmolem2  15967  fprodcl2lem  15982  fprodmul  15992  fprodrev  16009  moddvds  16297  dvdsflip  16350  bitsf1ocnv  16477  sadcaddlem  16490  bezoutlem2  16573  bezoutlem4  16575  dfgcd2  16579  lcmgcdlem  16639  crth  16811  hashgcdlem  16821  phisum  16823  pcqcl  16889  pcid  16906  pcneg  16907  prmpwdvds  16937  pockthg  16939  4sqlem11  16988  ramub2  17047  0ram  17053  prmgaplem7  17090  prmgaplem8  17091  setscom  17213  qusval  17588  initoeu1  18064  termoeu1  18071  setcinv  18143  funcestrcsetclem9  18203  funcsetcestrclem9  18218  fullsetcestrc  18221  1stfcl  18252  2ndfcl  18253  hofpropd  18323  isacs3lem  18599  mgmhmlin  18724  mndpsuppss  18790  frmdss2  18888  frmdup1  18889  mgm2nsgrplem2  18944  mulgdirlem  19135  mulgass  19141  0nsg  19199  cycsubgcl  19236  ghmmulg  19258  conjghm  19279  qusghm  19285  gsumwrev  19399  symg2bas  19424  symgfixelsi  19467  f1otrspeq  19479  psgnunilem2  19527  psgnunilem3  19528  odf1o2  19605  lsmhash  19737  efgtf  19754  efginvrel2  19759  efgredeu  19784  efgcpbllemb  19787  frgpuplem  19804  frgpup1  19807  ghmcyg  19928  gsumval3lem1  19937  gsumzres  19941  gsumzcl2  19942  gsumzf1o  19944  gsumzaddlem  19953  gsumconst  19966  gsumzmhm  19969  gsumzoppg  19976  gsum2d  20004  subgdmdprd  20068  pgpfac1lem3  20111  gsummgp0  20331  rnghmmul  20465  rngcinv  20653  ringcinv  20687  islmodd  20880  lmodvsmmulgdi  20911  islss3  20974  0lmhm  21056  idlmhm  21057  lmhmeql  21071  pwssplit3  21077  lidldvgen  21361  qsssubdrg  21461  cnsubrg  21462  znf1o  21587  psgnghm  21615  psgndif  21637  cssmre  21728  dsmmsubg  21780  frlmup1  21835  lindfrn  21858  f1lindf  21859  evlslem1  22123  psdmul  22187  coe1tmmul2  22294  pf1ind  22374  mamufval  22411  mamurid  22463  mvmulfval  22563  mdetralt2  22630  mndifsplit  22657  maducoeval2  22661  madugsum  22664  mat2pmatmul  22752  decpmatmul  22793  pm2mpf1lem  22815  pm2mpf1  22820  monmat2matmon  22845  chpscmat  22863  fvmptnn04if  22870  tgcl  22991  ppttop  23029  epttop  23031  clsval2  23073  opncldf1  23107  mretopd  23115  neindisj  23140  neiptopnei  23155  restcls  23204  restntr  23205  ordtbas  23215  cnpnei  23287  cncls2  23296  tgcmp  23424  cmpcld  23425  uncmp  23426  hauscmplem  23429  1stcfb  23468  2ndcctbss  23478  hauspwdom  23524  reftr  23537  comppfsc  23555  kgentopon  23561  ptpjpre1  23594  ptcnplem  23644  txcn  23649  txdis1cn  23658  txhaus  23670  xkopt  23678  imasnopn  23713  imasncld  23714  imasncls  23715  hmeoimaf1o  23793  cmphaushmeo  23823  txhmeo  23826  trfbas2  23866  fbasfip  23891  fbasrn  23907  fmss  23969  elfm2  23971  hauspwpwf1  24010  flfcnp  24027  fclscf  24048  flimfnfcls  24051  fcfval  24056  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  ptcmplem3  24077  ptcmplem4  24078  cnextfval  24085  cnextcn  24090  tmdgsum2  24119  ustex2sym  24240  neipcfilu  24320  imasdsf1olem  24398  metss2lem  24539  stdbdxmet  24543  stdbdmopn  24546  metrest  24552  metcnp  24569  restmetu  24598  tngngp  24690  icccmplem1  24857  icccvx  24994  evth  25004  lebnumlem1  25006  pi1blem  25085  isncvsngp  25196  equivcau  25347  bcthlem5  25375  cmslssbn  25419  ivthlem3  25501  ovolicc2lem3  25567  ovolicc2lem4  25568  dyaddisj  25644  dyadmbllem  25647  ismbfd  25687  itg2seq  25791  itgss  25861  limciun  25943  dvcobr  25997  dvcobrOLD  25998  dvmptfsum  26027  c1liplem1  26049  c1lip1  26050  lhop  26069  dvcvx  26073  tdeglem4  26113  plyco0  26245  elply2  26249  plypf1  26265  dgreq0  26319  elqaalem2  26376  aalioulem6  26393  aaliou  26394  aaliou2b  26397  ulmss  26454  ulmcn  26456  pserulm  26479  lgamgulmlem5  27090  basellem4  27141  fsumdvdsdiaglem  27240  mpodvdsmulf1o  27251  dvdsmulf1o  27253  chtublem  27269  fsumvma2  27272  logfaclbnd  27280  dchrelbasd  27297  lgsqrlem2  27405  gausslemma2dlem1a  27423  lgseisenlem2  27434  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  rplogsumlem2  27543  rpvmasumlem  27545  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasum2lem  27554  rpvmasum2  27570  dchrisum0lem1  27574  logsqvma  27600  selberg4  27619  pntibndlem3  27650  pntlem3  27667  ostthlem1  27685  ostthlem2  27686  sltres  27721  nogt01o  27755  oldbdayim  27941  addsproplem2  28017  negsproplem2  28075  mulsval  28149  om2noseqrdg  28324  noseqrdgfn  28326  zmulscld  28397  recut  28442  idmot  28559  brcgr  28929  brbtwn2  28934  axsegconlem8  28953  axpaschlem  28969  axeuclid  28992  axcontlem2  28994  axcontlem7  28999  eengtrkg  29015  upgrex  29123  subgrprop3  29307  subupgr  29318  nbgr0edglem  29387  nb3grprlem1  29411  cusgredg  29455  cusgrres  29480  usgredgsscusgredg  29491  finsumvtxdg2ssteplem4  29580  finsumvtxdg2sstep  29581  wlkl1loop  29670  wlkp1lem4  29708  wwlksnred  29921  wwlksnext  29922  wwlksnextwrd  29926  wpthswwlks2on  29990  clwwlknp  30065  clwwlkel  30074  wwlksext2clwwlk  30085  clwwlknonwwlknonb  30134  3wlkond  30199  1conngr  30222  eucrctshift  30271  fusgr2wsp2nb  30362  numclwwlk1lem2foa  30382  numclwwlk1lem2f1  30385  numclwlk1lem1  30397  numclwlk1lem2  30398  grpoidinvlem1  30532  grporcan  30546  ipblnfi  30883  hvmulcan2  31101  shscli  31345  spansneleq  31598  pjspansn  31605  3oalem2  31691  eigposi  31864  cnlnadjlem2  32096  stlesi  32269  mdslmd1lem1  32353  mdslmd1lem2  32354  cdj1i  32461  disjxpin  32607  nn0xmulclb  32781  xreceu  32888  txomap  33794  pstmxmet  33857  qqhghm  33950  qqhrhm  33951  measinblem  34200  cntmeas  34206  ballotlemsf1o  34494  bnj945  34765  bnj1110  34974  f1resveqaeq  35077  cvmopnlem  35262  cvmfolem  35263  cvmliftmolem2  35266  cvmlift2lem10  35296  satf00  35358  satffunlem2lem1  35388  satefvfmla0  35402  mrsubvrs  35506  wzel  35805  btwnconn1lem8  36075  btwnconn1lem9  36076  btwnconn1lem10  36077  btwnconn1lem11  36078  btwnconn1lem12  36079  finminlem  36300  nn0prpwlem  36304  fnessref  36339  refssfne  36340  fnemeet2  36349  consym1  36402  bj-finsumval0  37267  topdifinffinlem  37329  relowlssretop  37345  rdgeqoa  37352  fvineqsneu  37393  pibt2  37399  matunitlindflem1  37602  poimirlem28  37634  mblfinlem1  37643  mblfinlem3  37645  mblfinlem4  37646  ovoliunnfl  37648  mbfresfi  37652  mbfposadd  37653  itg2addnclem2  37658  itg2addnc  37660  ftc1anc  37687  frinfm  37721  fdc  37731  blssp  37742  sstotbnd  37761  isbnd2  37769  ssbnd  37774  prdstotbnd  37780  prdsbnd2  37781  ismtyres  37794  heibor1lem  37795  rrnequiv  37821  rngoisocnv  37967  crngohomfo  37992  pridlc3  38059  membpartlem19  38792  prter3  38863  ax12eq  38922  ax12el  38923  cvratlem  39403  islvol2aN  39574  4atlem4b  39582  4atlem4c  39583  4atlem4d  39584  isline2  39756  isline3  39758  pclfinclN  39932  linepsubclN  39933  pexmidlem4N  39955  diaglbN  41037  dvhvaddcl  41077  dvhvaddcomN  41078  dvhvscacl  41085  djavalN  41117  dibglbN  41148  dihatexv  41320  djhval  41380  mapdrvallem2  41627  metakunt15  42200  evlselvlem  42572  evlselv  42573  mhpind  42580  prjsprellsp  42597  elrfi  42681  nacsfix  42699  eldioph2  42749  lzenom  42757  rexrabdioph  42781  irrapxlem3  42811  pellexlem5  42820  pellex  42822  pell1234qrne0  42840  pell1234qrmulcl  42842  pell14qrdich  42856  pell1qrge1  42857  pellqrex  42866  rmxypairf1o  42899  rmxycomplete  42905  monotoddzzfi  42930  congadd  42954  jm2.19lem3  42979  jm2.19lem4  42980  jm2.25  42987  jm2.26a  42988  jm2.26lem3  42989  expdiophlem1  43009  wepwsolem  43030  lmhmfgsplit  43074  aaitgo  43150  mon1psubm  43187  deg1mhm  43188  succlg  43317  ofoacom  43350  iunrelexp0  43691  isotone2  44038  mnuprdlem4  44270  disjrnmpt2  45130  mullimc  45571  mullimcf  45578  climxrre  45705  fprodcncf  45855  stoweidlem17  45972  stoweidlem27  45982  stoweidlem54  46009  fourierdlem42  46104  fourierdlem62  46123  fourierdlem73  46134  fourierdlem76  46137  fourierdlem97  46158  sge0iunmptlemfi  46368  isomenndlem  46485  imarnf1pr  47231  smonoord  47295  fvelsetpreimafv  47311  iccpartiltu  47346  sprsymrelf1lem  47415  prproropf1olem3  47429  paireqne  47435  fmtnoprmfac1  47489  prmdvdsfmtnof1lem2  47509  uspgrimprop  47810  gricushgr  47823  grimedg  47840  rngcinvALTV  48119  funcringcsetcALTV2lem9  48141  ringcinvALTV  48153  funcringcsetclem9ALTV  48164  lmodvsmdi  48223  lincsum  48274  lindslinindimp2lem4  48306  nn0sumshdiglemB  48469  1arymaptf1  48491  2arymaptf1  48502  oduoppcciso  48881