Theorem ad2antll 765

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  simprr  796  simprrl  804  simprrr  805  prneimg  4388  fr2nr  5092  wereu2  5111  f1oprg  6181  fvtp1g  6463  funfvima3  6495  isof1oidb  6574  isomin  6587  weniso  6604  elovmpt3rab1  6893  sorpssi  6943  tfrlem9a  7482  oalimcl  7640  odi  7659  oeeui  7682  ralxpmap  7907  boxriin  7950  domdifsn  8043  domunsncan  8060  enfixsn  8069  disjen  8117  mapen  8124  mapxpen  8126  mapunen  8129  unxpdomlem2  8165  unxpdomlem3  8166  findcard2d  8202  findcard3  8203  isfinite2  8218  marypha1lem  8339  marypha2  8345  supmo  8358  infmo  8401  card2inf  8460  brwdom2  8478  wemapwe  8594  rankonidlem  8691  rankxplim3  8744  infxpenlem  8836  infxpenc2lem1  8842  infxpenc2  8845  fseqenlem1  8847  fseqenlem2  8848  infpwfien  8885  dfac12lem2  8966  infunsdom1  9035  infunsdom  9036  infmap2  9040  fin2i2  9140  fin23lem28  9162  fin23lem32  9166  fin23lem34  9168  fin23lem40  9173  isf32lem2  9176  compssiso  9196  isfin1-3  9208  fin1a2lem10  9231  fin12  9235  hsmexlem4  9251  ac6num  9301  ttukeylem7  9337  axdclem2  9342  iundom2g  9362  fpwwe2lem12  9463  pwfseqlem3  9482  winalim2  9518  winafp  9519  wunex2  9560  grur1  9642  dedekindle  10201  00id  10211  receu  10672  lt2mul2div  10901  peano5uzi  11466  uzwo  11751  qbtwnre  12030  iooshf  12252  modmul1  12723  seqcl2  12819  seqfveq2  12823  seqid2  12847  seqdistr  12852  expcl2lem  12872  mulexpz  12900  expnlbnd2  12995  hashfun  13224  hashfacen  13238  hashf1lem1  13239  elss2prb  13269  fstwrdne0  13345  swrdswrd  13460  wrd2ind  13477  splid  13504  repswrevw  13533  cshwidx0  13552  2cshw  13559  cshweqrep  13567  cshw1  13568  wwlktovfo  13701  relexpfld  13789  relexpindlem  13803  sqrlem6  13988  absexpz  14045  o1rlimmul  14349  iseralt  14415  summolem2  14447  fsumf1o  14454  fsum0diag2  14515  fsummulc2  14516  cvgcmpce  14550  incexclem  14568  prodmolem2  14665  fprodcl2lem  14680  fprodmul  14690  fprodrev  14707  moddvds  14991  dvdsflip  15039  bitsf1ocnv  15166  sadcaddlem  15179  bezoutlem2  15257  bezoutlem4  15259  dfgcd2  15263  lcmgcdlem  15319  crth  15483  hashgcdlem  15493  phisum  15495  pcqcl  15561  pcid  15577  pcneg  15578  prmpwdvds  15608  pockthg  15610  4sqlem11  15659  ramub2  15718  0ram  15724  prmgaplem7  15761  prmgaplem8  15762  setscom  15903  qusval  16202  initoeu1  16661  termoeu1  16668  setcinv  16740  funcestrcsetclem9  16788  funcsetcestrclem9  16803  fullsetcestrc  16806  1stfcl  16837  2ndfcl  16838  hofpropd  16907  isacs3lem  17166  frmdss2  17400  frmdup1  17401  mgm2nsgrplem2  17406  mulgdirlem  17572  mulgass  17579  cycsubgcl  17620  0nsg  17639  ghmmulg  17672  conjghm  17691  qusghm  17697  gsumwrev  17796  symg2bas  17818  symgfixelsi  17855  f1otrspeq  17867  psgnunilem2  17915  psgnunilem3  17916  odf1o2  17988  lsmhash  18118  efgtf  18135  efgredeu  18165  efgcpbllemb  18168  frgpuplem  18185  frgpup1  18188  cygabl  18292  ghmcyg  18297  gsumval3lem1  18306  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  gsum2d  18371  subgdmdprd  18433  pgpfac1lem3  18476  gsummgp0  18608  islmodd  18869  islss3  18959  0lmhm  19040  idlmhm  19041  lmhmeql  19055  pwssplit3  19061  lidldvgen  19255  evlslem1  19515  coe1tmmul2  19646  pf1ind  19719  qsssubdrg  19805  cnsubrg  19806  znf1o  19900  psgnghm  19926  psgndif  19948  cssmre  20037  dsmmsubg  20087  frlmup1  20137  lindfrn  20160  f1lindf  20161  mamufval  20191  mamurid  20248  mvmulfval  20348  mdetralt2  20415  mndifsplit  20442  maducoeval2  20446  madugsum  20449  mat2pmatmul  20536  decpmatmul  20577  pm2mpf1lem  20599  pm2mpf1  20604  monmat2matmon  20629  chpscmat  20647  fvmptnn04if  20654  tgcl  20773  ppttop  20811  epttop  20813  clsval2  20854  opncldf1  20888  mretopd  20896  neindisj  20921  neiptopnei  20936  restcls  20985  restntr  20986  ordtbas  20996  cnpnei  21068  cncls2  21077  tgcmp  21204  cmpcld  21205  uncmp  21206  hauscmplem  21209  1stcfb  21248  2ndcctbss  21258  hauspwdom  21304  reftr  21317  comppfsc  21335  kgentopon  21341  ptpjpre1  21374  ptcnplem  21424  txcn  21429  txdis1cn  21438  txhaus  21450  xkopt  21458  imasnopn  21493  imasncld  21494  imasncls  21495  hmeoimaf1o  21573  cmphaushmeo  21603  txhmeo  21606  trfbas2  21647  fbasfip  21672  fbasrn  21688  fmss  21750  elfm2  21752  hauspwpwf1  21791  flfcnp  21808  fclscf  21829  flimfnfcls  21832  fcfval  21837  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem3  21858  ptcmplem4  21859  cnextfval  21866  cnextcn  21871  tmdgsum2  21900  ustex2sym  22020  neipcfilu  22100  imasdsf1olem  22178  metss2lem  22316  stdbdxmet  22320  stdbdmopn  22323  metrest  22329  metcnp  22346  restmetu  22375  tngngp  22458  icccmplem1  22625  icccvx  22749  evth  22758  lebnumlem1  22760  pi1blem  22839  isncvsngp  22949  equivcau  23098  bcthlem5  23125  ivthlem3  23222  ovolicc2lem3  23287  ovolicc2lem4  23288  dyaddisj  23364  dyadmbllem  23367  ismbfd  23407  itg2seq  23509  itgss  23578  limciun  23658  dvcobr  23709  dvmptfsum  23738  c1liplem1  23759  c1lip1  23760  lhop  23779  dvcvx  23783  plyco0  23948  elply2  23952  plypf1  23968  dgreq0  24021  elqaalem2  24075  aalioulem6  24092  aaliou  24093  aaliou2b  24096  ulmss  24151  ulmcn  24153  pserulm  24176  lgamgulmlem5  24759  basellem4  24810  fsumdvdsdiaglem  24909  dvdsmulf1o  24920  chtublem  24936  fsumvma2  24939  logfaclbnd  24947  dchrelbasd  24964  lgsqrlem2  25072  gausslemma2dlem1a  25090  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  rplogsumlem2  25174  rpvmasumlem  25176  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  rpvmasum2  25201  dchrisum0lem1  25205  logsqvma  25231  selberg4  25250  pntibndlem3  25281  pntlem3  25298  ostthlem1  25316  ostthlem2  25317  idmot  25432  brcgr  25780  brbtwn2  25785  axsegconlem8  25804  axpaschlem  25820  axeuclid  25843  axcontlem2  25845  axcontlem7  25850  eengtrkg  25865  upgrex  25987  subgrprop3  26168  subupgr  26179  nbgr0vtxlem  26251  nb3grprlem1  26282  cusgredg  26320  cusgrres  26344  usgredgsscusgredg  26355  finsumvtxdg2ssteplem4  26444  finsumvtxdg2sstep  26445  wlkl1loop  26534  wlkp1lem4  26573  wwlksnred  26787  wwlksnext  26788  wwlksnextwrd  26792  wwlksnwwlksnon  26810  wpthswwlks2on  26854  clwwlksel  26914  wwlksext2clwwlk  26924  clwwnisshclwwsn  26930  clwlksfoclwwlk  26963  3wlkond  27031  1conngr  27054  eucrctshift  27103  fusgr2wsp2nb  27198  numclwlk1lem2f1  27227  numclwwlkqhash  27233  grpoidinvlem1  27358  grporcan  27372  ipblnfi  27711  hvmulcan2  27930  shscli  28176  spansneleq  28429  pjspansn  28436  3oalem2  28522  eigposi  28695  cnlnadjlem2  28927  stlesi  29100  mdslmd1lem1  29184  mdslmd1lem2  29185  cdj1i  29292  disjxpin  29401  xreceu  29630  txomap  29901  pstmxmet  29940  qqhghm  30032  qqhrhm  30033  measinblem  30283  cntmeas  30289  ballotlemsf1o  30575  bnj945  30844  bnj1110  31050  cvmopnlem  31260  cvmfolem  31261  cvmliftmolem2  31264  cvmlift2lem10  31294  mrsubvrs  31419  poseq  31750  wzel  31771  wzelOLD  31772  sltres  31815  sslttr  31914  btwnconn1lem8  32201  btwnconn1lem9  32202  btwnconn1lem10  32203  btwnconn1lem11  32204  btwnconn1lem12  32205  finminlem  32312  nn0prpwlem  32317  fnessref  32352  refssfne  32353  fnemeet2  32362  consym1  32419  bj-finsumval0  33147  topdifinffinlem  33195  relowlssretop  33211  rdgeqoa  33218  matunitlindflem1  33405  poimirlem28  33437  mblfinlem1  33446  mblfinlem3  33448  mblfinlem4  33449  ovoliunnfl  33451  mbfresfi  33456  mbfposadd  33457  itg2addnclem2  33462  itg2addnc  33464  ftc1anc  33493  frinfm  33530  fdc  33541  blssp  33552  sstotbnd  33574  isbnd2  33582  ssbnd  33587  prdstotbnd  33593  prdsbnd2  33594  ismtyres  33607  heibor1lem  33608  rrnequiv  33634  rngoisocnv  33780  crngohomfo  33805  pridlc3  33872  prter3  34167  ax12eq  34226  ax12el  34227  cvratlem  34707  islvol2aN  34878  4atlem4b  34886  4atlem4c  34887  4atlem4d  34888  isline2  35060  isline3  35062  pclfinclN  35236  linepsubclN  35237  pexmidlem4N  35259  diaglbN  36344  dvhvaddcl  36384  dvhvaddcomN  36385  dvhvscacl  36392  djavalN  36424  dibglbN  36455  dihatexv  36627  djhval  36687  mapdrvallem2  36934  elrfi  37257  nacsfix  37275  eldioph2  37325  lzenom  37333  rexrabdioph  37358  irrapxlem3  37388  pellexlem5  37397  pellex  37399  pell1234qrne0  37417  pell1234qrmulcl  37419  pell14qrdich  37433  pell1qrge1  37434  pellqrex  37443  rmxypairf1o  37476  rmxycomplete  37482  monotoddzzfi  37507  congadd  37533  jm2.19lem3  37558  jm2.19lem4  37559  jm2.25  37566  jm2.26a  37567  jm2.26lem3  37568  expdiophlem1  37588  wepwsolem  37612  lmhmfgsplit  37656  aaitgo  37732  mon1psubm  37784  deg1mhm  37785  iunrelexp0  37994  isotone2  38347  disjrnmpt2  39375  mullimc  39848  mullimcf  39855  climxrre  39982  fprodcncf  40114  stoweidlem17  40234  stoweidlem27  40244  stoweidlem54  40271  fourierdlem42  40366  fourierdlem62  40385  fourierdlem73  40396  fourierdlem76  40399  fourierdlem97  40420  sge0iunmptlemfi  40630  isomenndlem  40744  ovnsslelem  40774  imarnf1pr  41301  smonoord  41341  iccpartiltu  41358  ccatpfx  41409  fmtnoprmfac1  41477  prmdvdsfmtnof1lem2  41497  sprsymrelf1lem  41741  mgmhmlin  41786  rnghmmul  41900  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  funcringcsetcALTV2lem9  42044  ringcinvALTV  42056  funcringcsetclem9ALTV  42067  mndpsuppss  42152  lmodvsmdi  42163  lincsum  42218  lindslinindimp2lem4  42250  nn0sumshdiglemB  42414