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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  simprr  769  simprrl  777  simprrr  778  simprr1  1214  simprr2  1215  simprr3  1216  prneimg  4692  fr2nr  5421  wereu2  5440  f1oprg  6527  fvtp1g  6827  funfvima3  6863  isof1oidb  6940  isomin  6953  weniso  6970  elovmpt3rab1  7263  sorpssi  7313  suppofssd  7718  tfrlem9a  7874  oalimcl  8036  odi  8055  oeeui  8078  ralxpmap  8309  boxriin  8352  domdifsn  8447  domunsncan  8464  enfixsn  8473  disjen  8521  mapen  8528  mapxpen  8530  mapunen  8533  unxpdomlem2  8569  unxpdomlem3  8570  findcard2d  8606  findcard3  8607  isfinite2  8622  marypha1lem  8743  marypha2  8749  supmo  8762  infmo  8805  card2inf  8865  brwdom2  8883  wemapwe  9006  rankonidlem  9103  rankxplim3  9156  djulf1o  9187  djurf1o  9188  infxpenlem  9285  infxpenc2lem1  9291  infxpenc2  9294  fseqenlem1  9296  fseqenlem2  9297  infpwfien  9334  dfac12lem2  9416  infunsdom1  9481  infunsdom  9482  infmap2  9486  fin2i2  9586  fin23lem28  9608  fin23lem32  9612  fin23lem34  9614  fin23lem40  9619  isf32lem2  9622  compssiso  9642  isfin1-3  9654  fin1a2lem10  9677  fin12  9681  hsmexlem4  9697  ac6num  9747  ttukeylem7  9783  axdclem2  9788  iundom2g  9808  fpwwe2lem12  9909  pwfseqlem3  9928  winalim2  9964  winafp  9965  wunex2  10006  grur1  10088  dedekindle  10651  00id  10662  receu  11133  lt2mul2div  11366  peano5uzi  11920  uzwo  12160  qbtwnre  12442  iooshf  12665  modmul1  13142  seqcl2  13238  seqfveq2  13242  seqid2  13266  seqdistr  13271  expcl2lem  13291  mulexpz  13319  expnlbnd2  13445  hashfun  13646  hashfacen  13660  hashf1lem1  13661  elss2prb  13691  fstwrdne0  13754  swrdsb0eq  13861  ccatpfx  13899  swrdswrd  13903  wrd2ind  13921  splid  13951  repswrevw  13985  cshwidx0  14004  2cshw  14011  cshweqrep  14019  cshw1  14020  wwlktovfo  14156  relexpfld  14242  relexpindlem  14256  sqrlem6  14441  absexpz  14499  o1rlimmul  14809  iseralt  14875  summolem2  14906  fsumf1o  14913  fsum0diag2  14971  fsummulc2  14972  cvgcmpce  15006  incexclem  15024  prodmolem2  15122  fprodcl2lem  15137  fprodmul  15147  fprodrev  15164  moddvds  15451  dvdsflip  15500  bitsf1ocnv  15626  sadcaddlem  15639  bezoutlem2  15717  bezoutlem4  15719  dfgcd2  15723  lcmgcdlem  15779  crth  15944  hashgcdlem  15954  phisum  15956  pcqcl  16022  pcid  16038  pcneg  16039  prmpwdvds  16069  pockthg  16071  4sqlem11  16120  ramub2  16179  0ram  16185  prmgaplem7  16222  prmgaplem8  16223  setscom  16356  qusval  16644  initoeu1  17100  termoeu1  17107  setcinv  17179  funcestrcsetclem9  17227  funcsetcestrclem9  17242  fullsetcestrc  17245  1stfcl  17276  2ndfcl  17277  hofpropd  17346  isacs3lem  17605  frmdss2  17839  frmdup1  17840  mgm2nsgrplem2  17845  mulgdirlem  18012  mulgass  18018  cycsubgcl  18059  0nsg  18078  ghmmulg  18111  conjghm  18130  qusghm  18136  gsumwrev  18235  symg2bas  18257  symgfixelsi  18294  f1otrspeq  18306  psgnunilem2  18354  psgnunilem3  18355  odf1o2  18428  lsmhash  18558  efgtf  18575  efgredeu  18605  efgcpbllemb  18608  frgpuplem  18625  frgpup1  18628  cygabl  18732  ghmcyg  18737  gsumval3lem1  18746  gsumzres  18750  gsumzcl2  18751  gsumzf1o  18753  gsumzaddlem  18761  gsumconst  18774  gsumzmhm  18777  gsumzoppg  18784  gsum2d  18812  subgdmdprd  18873  pgpfac1lem3  18916  gsummgp0  19048  islmodd  19330  lmodvsmmulgdi  19359  islss3  19421  0lmhm  19502  idlmhm  19503  lmhmeql  19517  pwssplit3  19523  lidldvgen  19717  evlslem1  19982  coe1tmmul2  20127  pf1ind  20200  qsssubdrg  20286  cnsubrg  20287  znf1o  20380  psgnghm  20406  psgndif  20428  cssmre  20519  dsmmsubg  20569  frlmup1  20624  lindfrn  20647  f1lindf  20648  mamufval  20678  mamurid  20735  mvmulfval  20835  mdetralt2  20902  mndifsplit  20929  maducoeval2  20933  madugsum  20936  mat2pmatmul  21023  decpmatmul  21064  pm2mpf1lem  21086  pm2mpf1  21091  monmat2matmon  21116  chpscmat  21134  fvmptnn04if  21141  tgcl  21261  ppttop  21299  epttop  21301  clsval2  21342  opncldf1  21376  mretopd  21384  neindisj  21409  neiptopnei  21424  restcls  21473  restntr  21474  ordtbas  21484  cnpnei  21556  cncls2  21565  tgcmp  21693  cmpcld  21694  uncmp  21695  hauscmplem  21698  1stcfb  21737  2ndcctbss  21747  hauspwdom  21793  reftr  21806  comppfsc  21824  kgentopon  21830  ptpjpre1  21863  ptcnplem  21913  txcn  21918  txdis1cn  21927  txhaus  21939  xkopt  21947  imasnopn  21982  imasncld  21983  imasncls  21984  hmeoimaf1o  22062  cmphaushmeo  22092  txhmeo  22095  trfbas2  22135  fbasfip  22160  fbasrn  22176  fmss  22238  elfm2  22240  hauspwpwf1  22279  flfcnp  22296  fclscf  22317  flimfnfcls  22320  fcfval  22325  alexsubALTlem2  22340  alexsubALTlem3  22341  alexsubALTlem4  22342  ptcmplem3  22346  ptcmplem4  22347  cnextfval  22354  cnextcn  22359  tmdgsum2  22388  ustex2sym  22508  neipcfilu  22588  imasdsf1olem  22666  metss2lem  22804  stdbdxmet  22808  stdbdmopn  22811  metrest  22817  metcnp  22834  restmetu  22863  tngngp  22946  icccmplem1  23113  icccvx  23237  evth  23246  lebnumlem1  23248  pi1blem  23326  isncvsngp  23436  equivcau  23586  bcthlem5  23614  cmslssbn  23658  ivthlem3  23737  ovolicc2lem3  23803  ovolicc2lem4  23804  dyaddisj  23880  dyadmbllem  23883  ismbfd  23923  itg2seq  24026  itgss  24095  limciun  24175  dvcobr  24226  dvmptfsum  24255  c1liplem1  24276  c1lip1  24277  lhop  24296  dvcvx  24300  plyco0  24465  elply2  24469  plypf1  24485  dgreq0  24538  elqaalem2  24592  aalioulem6  24609  aaliou  24610  aaliou2b  24613  ulmss  24668  ulmcn  24670  pserulm  24693  lgamgulmlem5  25292  basellem4  25343  fsumdvdsdiaglem  25442  dvdsmulf1o  25453  chtublem  25469  fsumvma2  25472  logfaclbnd  25480  dchrelbasd  25497  lgsqrlem2  25605  gausslemma2dlem1a  25623  lgseisenlem2  25634  lgsquadlem1  25638  lgsquadlem2  25639  lgsquadlem3  25640  rplogsumlem2  25743  rpvmasumlem  25745  dchrmusum2  25752  dchrvmasumlem1  25753  dchrvmasum2lem  25754  rpvmasum2  25770  dchrisum0lem1  25774  logsqvma  25800  selberg4  25819  pntibndlem3  25850  pntlem3  25867  ostthlem1  25885  ostthlem2  25886  idmot  26005  brcgr  26369  brbtwn2  26374  axsegconlem8  26393  axpaschlem  26409  axeuclid  26432  axcontlem2  26434  axcontlem7  26439  eengtrkg  26455  upgrex  26560  subgrprop3  26741  subupgr  26752  nbgr0vtxlem  26820  nb3grprlem1  26845  cusgredg  26889  cusgrres  26913  usgredgsscusgredg  26924  finsumvtxdg2ssteplem4  27013  finsumvtxdg2sstep  27014  wlkl1loop  27102  wlkp1lem4  27143  wwlksnred  27357  wwlksnext  27358  wwlksnextwrd  27362  wpthswwlks2on  27427  clwwlknp  27502  clwwlkel  27512  wwlksext2clwwlk  27523  clwwlknonwwlknonb  27572  3wlkond  27637  1conngr  27660  eucrctshift  27710  fusgr2wsp2nb  27805  numclwwlk1lem2foa  27825  numclwwlk1lem2f1  27828  numclwlk1lem1  27840  numclwlk1lem2  27841  grpoidinvlem1  27972  grporcan  27986  ipblnfi  28323  hvmulcan2  28541  shscli  28785  spansneleq  29038  pjspansn  29045  3oalem2  29131  eigposi  29304  cnlnadjlem2  29536  stlesi  29709  mdslmd1lem1  29793  mdslmd1lem2  29794  cdj1i  29901  disjxpin  30028  nn0xmulclb  30184  xreceu  30282  txomap  30715  pstmxmet  30754  qqhghm  30846  qqhrhm  30847  measinblem  31096  cntmeas  31102  ballotlemsf1o  31388  bnj945  31662  bnj1110  31868  f1resveqaeq  31972  cvmopnlem  32133  cvmfolem  32134  cvmliftmolem2  32137  cvmlift2lem10  32167  satf00  32229  satffunlem2lem1  32259  satefvfmla0  32273  mrsubvrs  32377  poseq  32704  wzel  32720  sltres  32778  sslttr  32877  btwnconn1lem8  33164  btwnconn1lem9  33165  btwnconn1lem10  33166  btwnconn1lem11  33167  btwnconn1lem12  33168  finminlem  33275  nn0prpwlem  33279  fnessref  33314  refssfne  33315  fnemeet2  33324  consym1  33377  bj-finsumval0  34119  topdifinffinlem  34159  relowlssretop  34175  rdgeqoa  34182  fvineqsneu  34223  pibt2  34229  matunitlindflem1  34419  poimirlem28  34451  mblfinlem1  34460  mblfinlem3  34462  mblfinlem4  34463  ovoliunnfl  34465  mbfresfi  34469  mbfposadd  34470  itg2addnclem2  34475  itg2addnc  34477  ftc1anc  34506  frinfm  34542  fdc  34552  blssp  34563  sstotbnd  34585  isbnd2  34593  ssbnd  34598  prdstotbnd  34604  prdsbnd2  34605  ismtyres  34618  heibor1lem  34619  rrnequiv  34645  rngoisocnv  34791  crngohomfo  34816  pridlc3  34883  prter3  35549  ax12eq  35608  ax12el  35609  cvratlem  36088  islvol2aN  36259  4atlem4b  36267  4atlem4c  36268  4atlem4d  36269  isline2  36441  isline3  36443  pclfinclN  36617  linepsubclN  36618  pexmidlem4N  36640  diaglbN  37722  dvhvaddcl  37762  dvhvaddcomN  37763  dvhvscacl  37770  djavalN  37802  dibglbN  37833  dihatexv  38005  djhval  38065  mapdrvallem2  38312  prjsprellsp  38758  elrfi  38776  nacsfix  38794  eldioph2  38844  lzenom  38852  rexrabdioph  38876  irrapxlem3  38906  pellexlem5  38915  pellex  38917  pell1234qrne0  38935  pell1234qrmulcl  38937  pell14qrdich  38951  pell1qrge1  38952  pellqrex  38961  rmxypairf1o  38993  rmxycomplete  38999  monotoddzzfi  39024  congadd  39048  jm2.19lem3  39073  jm2.19lem4  39074  jm2.25  39081  jm2.26a  39082  jm2.26lem3  39083  expdiophlem1  39103  wepwsolem  39127  lmhmfgsplit  39171  aaitgo  39247  mon1psubm  39291  deg1mhm  39292  iunrelexp0  39532  isotone2  39884  mnuprdlem4  40108  disjrnmpt2  40989  mullimc  41439  mullimcf  41446  climxrre  41573  fprodcncf  41725  stoweidlem17  41844  stoweidlem27  41854  stoweidlem54  41881  fourierdlem42  41976  fourierdlem62  41995  fourierdlem73  42006  fourierdlem76  42009  fourierdlem97  42030  sge0iunmptlemfi  42237  isomenndlem  42354  ovnsslelem  42384  imarnf1pr  42997  smonoord  43047  iccpartiltu  43064  sprsymrelf1lem  43135  prproropf1olem3  43149  paireqne  43155  fmtnoprmfac1  43209  prmdvdsfmtnof1lem2  43229  isomushgr  43473  isomuspgrlem2c  43477  mgmhmlin  43535  rnghmmul  43649  rngcinv  43730  rngcinvALTV  43742  ringcinv  43781  funcringcsetcALTV2lem9  43793  ringcinvALTV  43805  funcringcsetclem9ALTV  43816  mndpsuppss  43899  lmodvsmdi  43910  lincsum  43964  lindslinindimp2lem4  43996  nn0sumshdiglemB  44161