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  772  simprrl  780  simprrr  781  simprr1  1222  simprr2  1223  simprr3  1224  prneimg  4810  prproe  4861  fr2nr  5601  wereu2  5621  f1oprg  6820  fvtp1g  7144  funfvima3  7182  isof1oidb  7270  isomin  7283  weniso  7300  elovmpt3rab1  7618  sorpssi  7674  resf1extb  7876  poseq  8100  suppofssd  8145  tfrlem9a  8317  oalimcl  8487  odi  8506  oeeui  8530  ralxpmap  8836  boxriin  8880  domdifsn  8990  domunsncan  9007  enfixsn  9016  disjen  9064  mapen  9071  mapxpen  9073  mapunen  9076  findcard2d  9093  unxpdomlem2  9159  unxpdomlem3  9160  isfinite2  9200  marypha1lem  9338  marypha2  9344  supmo  9357  infmo  9402  card2inf  9462  brwdom2  9480  wemapwe  9608  rankonidlem  9742  rankxplim3  9795  djulf1o  9826  djurf1o  9827  infxpenlem  9925  infxpenc2lem1  9931  infxpenc2  9934  fseqenlem1  9936  fseqenlem2  9937  infpwfien  9974  dfac12lem2  10057  infunsdom1  10124  infunsdom  10125  infmap2  10129  fin2i2  10230  fin23lem28  10252  fin23lem32  10256  fin23lem34  10258  fin23lem40  10263  isf32lem2  10266  compssiso  10286  isfin1-3  10298  fin1a2lem10  10321  fin12  10325  hsmexlem4  10341  ac6num  10391  ttukeylem7  10427  axdclem2  10432  iundom2g  10452  fpwwe2lem11  10554  pwfseqlem3  10573  winalim2  10609  winafp  10610  wunex2  10651  grur1  10733  dedekindle  11299  00id  11310  receu  11784  lt2mul2div  12022  peano5uzi  12583  uzwo  12826  qbtwnre  13116  iooshf  13344  modmul1  13849  seqcl2  13945  seqfveq2  13949  seqid2  13973  seqdistr  13978  expcl2lem  13998  mulexpz  14027  expnlbnd2  14159  hashfun  14362  hashfacen  14379  hashf1lem1  14380  elss2prb  14413  fstwrdne0  14481  swrdsb0eq  14589  swrdswrd  14630  wrd2ind  14648  swrdccatin1  14650  pfxccatin12  14658  splid  14678  repswrevw  14712  cshwidxmod  14728  cshwidx0  14731  2cshw  14738  cshweqrep  14746  cshw1  14747  wwlktovfo  14883  relexpfld  14974  relexpindlem  14988  01sqrexlem6  15172  absexpz  15230  o1rlimmul  15544  iseralt  15610  summolem2  15641  fsumf1o  15648  fsum0diag2  15708  fsummulc2  15709  cvgcmpce  15743  incexclem  15761  prodmolem2  15860  fprodcl2lem  15875  fprodmul  15885  fprodrev  15902  moddvds  16192  dvdsflip  16246  bitsf1ocnv  16373  sadcaddlem  16386  bezoutlem2  16469  bezoutlem4  16471  dfgcd2  16475  lcmgcdlem  16535  crth  16707  hashgcdlem  16717  phisum  16720  pcqcl  16786  pcid  16803  pcneg  16804  prmpwdvds  16834  pockthg  16836  4sqlem11  16885  ramub2  16944  0ram  16950  prmgaplem7  16987  prmgaplem8  16988  setscom  17109  qusval  17465  initoeu1  17937  termoeu1  17944  setcinv  18016  funcestrcsetclem9  18073  funcsetcestrclem9  18088  fullsetcestrc  18091  1stfcl  18122  2ndfcl  18123  hofpropd  18192  isacs3lem  18467  mgmhmlin  18626  mndpsuppss  18692  frmdss2  18790  frmdup1  18791  mgm2nsgrplem2  18846  mulgdirlem  19037  mulgass  19043  0nsg  19100  cycsubgcl  19137  ghmmulg  19159  conjghm  19180  qusghm  19186  gsumwrev  19297  symg2bas  19324  symgfixelsi  19366  f1otrspeq  19378  psgnunilem2  19426  psgnunilem3  19427  odf1o2  19504  lsmhash  19636  efgtf  19653  efginvrel2  19658  efgredeu  19683  efgcpbllemb  19686  frgpuplem  19703  frgpup1  19706  ghmcyg  19827  gsumval3lem1  19836  gsumzres  19840  gsumzcl2  19841  gsumzf1o  19843  gsumzaddlem  19852  gsumconst  19865  gsumzmhm  19868  gsumzoppg  19875  gsum2d  19903  subgdmdprd  19967  pgpfac1lem3  20010  gsummgp0  20255  rnghmmul  20387  rngcinv  20572  ringcinv  20606  islmodd  20819  lmodvsmmulgdi  20850  islss3  20912  0lmhm  20994  idlmhm  20995  lmhmeql  21009  pwssplit3  21015  lidldvgen  21291  qsssubdrg  21383  cnsubrg  21384  znf1o  21508  psgnghm  21537  psgndif  21559  cssmre  21650  dsmmsubg  21700  frlmup1  21755  lindfrn  21778  f1lindf  21779  evlslem1  22039  psdmul  22111  coe1tmmul2  22220  pf1ind  22301  mamufval  22338  mamurid  22388  mvmulfval  22488  mdetralt2  22555  mndifsplit  22582  maducoeval2  22586  madugsum  22589  mat2pmatmul  22677  decpmatmul  22718  pm2mpf1lem  22740  pm2mpf1  22745  monmat2matmon  22770  chpscmat  22788  fvmptnn04if  22795  tgcl  22915  ppttop  22953  epttop  22955  clsval2  22996  opncldf1  23030  mretopd  23038  neindisj  23063  neiptopnei  23078  restcls  23127  restntr  23128  ordtbas  23138  cnpnei  23210  cncls2  23219  tgcmp  23347  cmpcld  23348  uncmp  23349  hauscmplem  23352  1stcfb  23391  2ndcctbss  23401  hauspwdom  23447  reftr  23460  comppfsc  23478  kgentopon  23484  ptpjpre1  23517  ptcnplem  23567  txcn  23572  txdis1cn  23581  txhaus  23593  xkopt  23601  imasnopn  23636  imasncld  23637  imasncls  23638  hmeoimaf1o  23716  cmphaushmeo  23746  txhmeo  23749  trfbas2  23789  fbasfip  23814  fbasrn  23830  fmss  23892  elfm2  23894  hauspwpwf1  23933  flfcnp  23950  fclscf  23971  flimfnfcls  23974  fcfval  23979  alexsubALTlem2  23994  alexsubALTlem3  23995  alexsubALTlem4  23996  ptcmplem3  24000  ptcmplem4  24001  cnextfval  24008  cnextcn  24013  tmdgsum2  24042  ustex2sym  24163  neipcfilu  24241  imasdsf1olem  24319  metss2lem  24457  stdbdxmet  24461  stdbdmopn  24464  metrest  24470  metcnp  24487  restmetu  24516  tngngp  24600  icccmplem1  24769  icccvx  24906  evth  24916  lebnumlem1  24918  pi1blem  24997  isncvsngp  25107  equivcau  25258  bcthlem5  25286  cmslssbn  25330  ivthlem3  25412  ovolicc2lem3  25478  ovolicc2lem4  25479  dyaddisj  25555  dyadmbllem  25558  ismbfd  25598  itg2seq  25701  itgss  25771  limciun  25853  dvcobr  25907  dvcobrOLD  25908  dvmptfsum  25937  c1liplem1  25959  c1lip1  25960  lhop  25979  dvcvx  25983  tdeglem4  26023  plyco0  26155  elply2  26159  plypf1  26175  dgreq0  26229  elqaalem2  26286  aalioulem6  26303  aaliou  26304  aaliou2b  26307  ulmss  26364  ulmcn  26366  pserulm  26389  lgamgulmlem5  27001  basellem4  27052  fsumdvdsdiaglem  27151  mpodvdsmulf1o  27162  dvdsmulf1o  27164  chtublem  27180  fsumvma2  27183  logfaclbnd  27191  dchrelbasd  27208  lgsqrlem2  27316  gausslemma2dlem1a  27334  lgseisenlem2  27345  lgsquadlem1  27349  lgsquadlem2  27350  lgsquadlem3  27351  rplogsumlem2  27454  rpvmasumlem  27456  dchrmusum2  27463  dchrvmasumlem1  27464  dchrvmasum2lem  27465  rpvmasum2  27481  dchrisum0lem1  27485  logsqvma  27511  selberg4  27530  pntibndlem3  27561  pntlem3  27578  ostthlem1  27596  ostthlem2  27597  ltsres  27632  nogt01o  27666  oldbdayim  27887  addsproplem2  27968  negsproplem2  28027  mulsval  28107  om2noseqrdg  28302  noseqrdgfn  28304  zmulscld  28395  recut  28492  idmot  28611  brcgr  28975  brbtwn2  28980  axsegconlem8  28999  axpaschlem  29015  axeuclid  29038  axcontlem2  29040  axcontlem7  29045  eengtrkg  29061  upgrex  29167  subgrprop3  29351  subupgr  29362  nbgr0edglem  29431  nb3grprlem1  29455  cusgredg  29499  cusgrres  29524  usgredgsscusgredg  29535  finsumvtxdg2ssteplem4  29624  finsumvtxdg2sstep  29625  wlkl1loop  29713  wlkp1lem4  29750  wwlksnred  29967  wwlksnext  29968  wwlksnextwrd  29972  wpthswwlks2on  30039  clwwlknp  30114  clwwlkel  30123  wwlksext2clwwlk  30134  clwwlknonwwlknonb  30183  3wlkond  30248  1conngr  30271  eucrctshift  30320  fusgr2wsp2nb  30411  numclwwlk1lem2foa  30431  numclwwlk1lem2f1  30434  numclwlk1lem1  30446  numclwlk1lem2  30447  grpoidinvlem1  30581  grporcan  30595  ipblnfi  30932  hvmulcan2  31150  shscli  31394  spansneleq  31647  pjspansn  31654  3oalem2  31740  eigposi  31913  cnlnadjlem2  32145  stlesi  32318  mdslmd1lem1  32402  mdslmd1lem2  32403  cdj1i  32510  disjxpin  32665  nn0xmulclb  32853  xreceu  33005  txomap  33993  pstmxmet  34056  qqhghm  34147  qqhrhm  34148  measinblem  34379  cntmeas  34385  ballotlemsf1o  34673  bnj945  34931  bnj1110  35140  f1resveqaeq  35243  rankfilimbi  35259  cvmopnlem  35474  cvmfolem  35475  cvmliftmolem2  35478  cvmlift2lem10  35508  satf00  35570  satffunlem2lem1  35600  satefvfmla0  35614  mrsubvrs  35718  wzel  36018  btwnconn1lem8  36290  btwnconn1lem9  36291  btwnconn1lem10  36292  btwnconn1lem11  36293  btwnconn1lem12  36294  finminlem  36514  nn0prpwlem  36518  fnessref  36553  refssfne  36554  fnemeet2  36563  consym1  36616  bj-finsumval0  37492  topdifinffinlem  37554  relowlssretop  37570  rdgeqoa  37577  fvineqsneu  37618  pibt2  37624  matunitlindflem1  37819  poimirlem28  37851  mblfinlem1  37860  mblfinlem3  37862  mblfinlem4  37863  ovoliunnfl  37865  mbfresfi  37869  mbfposadd  37870  itg2addnclem2  37875  itg2addnc  37877  ftc1anc  37904  frinfm  37938  fdc  37948  blssp  37959  sstotbnd  37978  isbnd2  37986  ssbnd  37991  prdstotbnd  37997  prdsbnd2  37998  ismtyres  38011  heibor1lem  38012  rrnequiv  38038  rngoisocnv  38184  crngohomfo  38209  pridlc3  38276  membpartlem19  39092  prter3  39164  ax12eq  39223  ax12el  39224  cvratlem  39703  islvol2aN  39874  4atlem4b  39882  4atlem4c  39883  4atlem4d  39884  isline2  40056  isline3  40058  pclfinclN  40232  linepsubclN  40233  pexmidlem4N  40255  diaglbN  41337  dvhvaddcl  41377  dvhvaddcomN  41378  dvhvscacl  41385  djavalN  41417  dibglbN  41448  dihatexv  41620  djhval  41680  mapdrvallem2  41927  evlselvlem  42850  evlselv  42851  mhpind  42858  prjsprellsp  42875  elrfi  42957  nacsfix  42975  eldioph2  43025  lzenom  43033  rexrabdioph  43057  irrapxlem3  43087  pellexlem5  43096  pellex  43098  pell1234qrne0  43116  pell1234qrmulcl  43118  pell14qrdich  43132  pell1qrge1  43133  pellqrex  43142  rmxypairf1o  43174  rmxycomplete  43180  monotoddzzfi  43205  congadd  43229  jm2.19lem3  43254  jm2.19lem4  43255  jm2.25  43262  jm2.26a  43263  jm2.26lem3  43264  expdiophlem1  43284  wepwsolem  43305  lmhmfgsplit  43349  aaitgo  43425  mon1psubm  43462  deg1mhm  43463  succlg  43591  ofoacom  43624  iunrelexp0  43964  isotone2  44311  mnuprdlem4  44537  relpmin  45214  disjrnmpt2  45453  mullimc  45883  mullimcf  45890  climxrre  46015  fprodcncf  46165  stoweidlem17  46282  stoweidlem27  46292  stoweidlem54  46319  fourierdlem42  46414  fourierdlem62  46433  fourierdlem73  46444  fourierdlem76  46447  fourierdlem97  46468  sge0iunmptlemfi  46678  isomenndlem  46795  imarnf1pr  47549  smonoord  47638  fvelsetpreimafv  47654  iccpartiltu  47689  sprsymrelf1lem  47758  prproropf1olem3  47772  paireqne  47778  fmtnoprmfac1  47832  prmdvdsfmtnof1lem2  47852  gricushgr  48184  grimedg  48202  cycl3grtri  48214  gpgedg2iv  48334  pgnbgreunbgrlem2lem1  48381  pgnbgreunbgrlem2lem2  48382  rngcinvALTV  48543  funcringcsetcALTV2lem9  48565  ringcinvALTV  48577  funcringcsetclem9ALTV  48588  lmodvsmdi  48646  lincsum  48696  lindslinindimp2lem4  48728  nn0sumshdiglemB  48887  1arymaptf1  48909  2arymaptf1  48920  dmrnxp  49103  xpco2  49123  initopropd  49509  termopropd  49510  zeroopropd  49511  oduoppcciso  49832  lanpropd  49881  ranpropd  49882