Theorem ad2antll 742

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simprr  785  simprrl  793  simprrr  794  simprr1  1240  simprr2  1241  simprr3  1242  prneimg  4817  prproe  4868  fr2nr  5636  wereu2  5656  f1oprg  6868  fvtp1g  7200  funfvima3  7239  f1resveqaeq  7274  isof1oidb  7329  isomin  7342  weniso  7361  elovmpt3rab1  7678  sorpssi  7734  resf1extb  7935  poseq  8160  suppofssd  8205  tfrlem9a  8379  oalimcl  8551  odi  8570  oeeui  8594  ralxpmap  8907  boxriin  8951  domdifsn  9062  domunsncan  9079  enfixsn  9088  disjen  9136  mapen  9143  mapxpen  9145  mapunen  9148  findcard2d  9165  unxpdomlem2  9231  unxpdomlem3  9232  isfinite2  9272  marypha1lem  9407  marypha2  9413  supmo  9426  infmo  9471  card2inf  9531  brwdom2  9549  wemapwe  9680  rankonidlem  9814  rankxplim3  9867  djulf1o  9921  djurf1o  9922  infxpenlem  10020  infxpenc2lem1  10026  infxpenc2  10029  fseqenlem1  10031  fseqenlem2  10032  infpwfien  10069  dfac12lem2  10151  infunsdom1  10218  infunsdom  10219  infmap2  10223  fin2i2  10324  fin23lem28  10346  fin23lem32  10350  fin23lem34  10352  fin23lem40  10357  isf32lem2  10360  compssiso  10380  isfin1-3  10392  fin1a2lem10  10415  fin12  10419  hsmexlem4  10435  ac6num  10485  ttukeylem7  10521  axdclem2  10526  iundom2g  10552  fpwwe2lem11  10654  pwfseqlem3  10673  winalim2  10709  winafp  10710  wunex2  10751  grur1  10833  dedekindle  11402  00id  11413  receu  11887  lt2mul2div  12121  peano5uzi  12714  uzwo  12964  qbtwnre  13255  iooshf  13483  modmul1  13992  seqcl2  14088  seqfveq2  14092  seqid2  14116  seqdistr  14121  expcl2lem  14141  mulexpz  14170  expnlbnd2  14302  hashfun  14506  hashfacen  14523  hashf1lem1  14524  elss2prb  14557  fstwrdne0  14625  swrdsb0eq  14737  swrdswrd  14778  wrd2ind  14796  swrdccatin1  14798  pfxccatin12  14806  splid  14826  repswrevw  14862  cshwidxmod  14878  cshwidx0  14881  2cshw  14888  cshweqrep  14896  cshw1  14897  wwlktovfo  15035  relexpfld  15126  relexpindlem  15140  01sqrexlem6  15338  absexpz  15396  o1rlimmul  15710  iseralt  15776  summolem2  15806  fsumf1o  15813  fsum0diag2  15873  fsummulc2  15874  cvgcmpce  15909  incexclem  15929  prodmolem2  16028  fprodcl2lem  16043  fprodmul  16053  fprodrev  16070  moddvds  16359  dvdsflip  16413  bitsf1ocnv  16540  sadcaddlem  16553  bezoutlem2  16636  bezoutlem4  16638  dfgcd2  16642  lcmgcdlem  16702  crth  16875  hashgcdlem  16885  phisum  16888  pcqcl  16954  pcid  16971  pcneg  16972  prmpwdvds  17002  pockthg  17004  4sqlem11  17053  ramub2  17112  0ram  17118  prmgaplem7  17155  prmgaplem8  17156  setscom  17278  qusval  17634  initoeu1  18106  termoeu1  18113  setcinv  18185  funcestrcsetclem9  18242  funcsetcestrclem9  18257  fullsetcestrc  18260  1stfcl  18291  2ndfcl  18292  hofpropd  18361  isacs3lem  18636  mgmhmlin  18807  mndpsuppss  18878  frmdss2  18978  frmdup1  18979  mgm2nsgrplem2  19037  mulgdirlem  19234  mulgass  19240  0nsg  19298  cycsubgcl  19340  ghmmulg  19361  conjghm  19382  qusghm  19388  gsumwrev  19499  symg2bas  19526  symgfixelsi  19568  f1otrspeq  19580  psgnunilem2  19628  psgnunilem3  19629  odf1o2  19706  lsmhash  19838  efgtf  19855  efginvrel2  19860  efgredeu  19885  efgcpbllemb  19888  frgpuplem  19905  frgpup1  19908  ghmcyg  20029  gsumval3lem1  20038  gsumzres  20042  gsumzcl2  20043  gsumzf1o  20045  gsumzaddlem  20054  gsumconst  20067  gsumzmhm  20070  gsumzoppg  20077  gsum2d  20105  subgdmdprd  20169  pgpfac1lem3  20212  gsummgp0  20464  rnghmmul  20596  rngcinv  20805  ringcinv  20839  islmodd  21056  lmodvsmmulgdi  21087  islss3  21149  0lmhm  21230  idlmhm  21231  lmhmeql  21245  pwssplit3  21251  cmprmidlmcl  21544  lidldvgen  21571  qsssubdrg  21645  cnsubrg  21646  znf1o  21770  psgnghm  21799  psgndif  21821  cssmre  21912  dsmmsubg  21962  frlmup1  22017  lindfrn  22040  f1lindf  22041  evlslem1  22304  psdmul  22400  coe1tmmul2  22508  pf1ind  22586  mamufval  22620  mamurid  22670  mvmulfval  22770  mdetralt2  22837  mndifsplit  22864  maducoeval2  22868  madugsum  22871  matunitlindflem1  22907  mat2pmatmul  22962  decpmatmul  23003  pm2mpf1lem  23025  pm2mpf1  23030  monmat2matmon  23055  chpscmat  23073  fvmptnn04if  23080  tgcl  23200  ppttop  23238  epttop  23240  clsval2  23281  opncldf1  23315  mretopd  23323  neindisj  23348  neiptopnei  23363  restcls  23412  restntr  23413  ordtbas  23423  cnpnei  23495  cncls2  23504  tgcmp  23632  cmpcld  23633  uncmp  23634  hauscmplem  23637  1stcfb  23676  2ndcctbss  23687  hauspwdom  23733  reftr  23746  comppfsc  23764  kgentopon  23770  ptpjpre1  23803  ptcnplem  23853  txcn  23858  txdis1cn  23867  txhaus  23879  xkopt  23887  imasnopn  23922  imasncld  23923  imasncls  23924  hmeoimaf1o  24002  cmphaushmeo  24032  txhmeo  24035  trfbas2  24075  fbasfip  24100  fbasrn  24116  fmss  24178  elfm2  24180  hauspwpwf1  24219  flfcnp  24236  fclscf  24257  flimfnfcls  24260  fcfval  24265  alexsubALTlem2  24280  alexsubALTlem3  24281  alexsubALTlem4  24282  ptcmplem3  24286  ptcmplem4  24287  cnextfval  24294  cnextcn  24299  tmdgsum2  24328  ustex2sym  24449  neipcfilu  24527  imasdsf1olem  24605  metss2lem  24743  stdbdxmet  24747  stdbdmopn  24750  metrest  24756  metcnp  24773  restmetu  24802  tngngp  24886  icccmplem1  25055  icccvx  25184  evth  25193  lebnumlem1  25195  pi1blem  25273  isncvsngp  25383  equivcau  25534  bcthlem5  25562  cmslssbn  25606  ivthlem3  25687  ovolicc2lem3  25753  ovolicc2lem4  25754  dyaddisj  25830  dyadmbllem  25833  ismbfd  25873  itg2seq  25976  itgss  26046  limciun  26128  dvcobr  26180  dvmptfsum  26209  c1liplem1  26230  c1lip1  26231  lhop  26250  dvcvx  26254  tdeglem4  26292  plyco0  26424  elply2  26428  plypf1  26445  dgreq0  26498  elqaalem2  26559  aalioulem6  26580  aaliou  26581  aaliou2b  26584  ulmss  26640  ulmcn  26642  pserulm  26665  lgamgulmlem5  27277  basellem4  27328  fsumdvdsdiaglem  27427  mpodvdsmulf1o  27438  dvdsmulf1o  27440  chtublem  27455  fsumvma2  27458  logfaclbnd  27466  dchrelbasd  27483  lgsqrlem2  27591  gausslemma2dlem1a  27609  lgseisenlem2  27620  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  rplogsumlem2  27729  rpvmasumlem  27731  dchrmusum2  27738  dchrvmasumlem1  27739  dchrvmasum2lem  27740  rpvmasum2  27756  dchrisum0lem1  27760  logsqvma  27786  selberg4  27805  pntibndlem3  27836  pntlem3  27853  ostthlem1  27871  ostthlem2  27872  ltsres  27906  nogt01o  27940  oldbdayim  28162  addsproplem2  28243  negsproplem2  28302  mulsval  28382  om2noseqrdg  28577  noseqrdgfn  28579  zmulscld  28670  recut  28767  idmot  28887  brcgr  29365  brbtwn2  29370  axsegconlem8  29389  axpaschlem  29405  axeuclid  29428  axcontlem2  29430  axcontlem7  29435  eengtrkg  29451  upgrex  29557  subgrprop3  29744  subupgr  29755  nbgr0edglem  29824  nb3grprlem1  29848  cusgredg  29892  cusgrres  29916  usgredgsscusgredg  29927  finsumvtxdg2ssteplem4  30016  finsumvtxdg2sstep  30017  wlkl1loop  30105  wlkp1lem4  30142  wwlksnred  30368  wwlksnext  30369  wwlksnextwrd  30373  wpthswwlks2on  30440  clwwlknp  30515  clwwlkel  30524  wwlksext2clwwlk  30535  clwwlknonwwlknonb  30584  3wlkond  30659  1conngr  30682  eucrctshift  30731  fusgr2wsp2nb  30822  numclwwlk1lem2foa  30842  numclwwlk1lem2f1  30845  numclwlk1lem1  30857  numclwlk1lem2  30858  grpoidinvlem1  30993  grporcan  31007  ipblnfi  31344  hvmulcan2  31562  shscli  31806  spansneleq  32059  pjspansn  32066  3oalem2  32152  eigposi  32325  cnlnadjlem2  32557  stlesi  32730  mdslmd1lem1  32814  mdslmd1lem2  32815  cdj1i  32922  disjxpin  33069  nn0xmulclb  33250  xreceu  33375  txomap  34352  pstmxmet  34415  qqhghm  34506  qqhrhm  34507  measinblem  34739  cntmeas  34745  ballotlemsf1o  35033  bnj945  35291  bnj1110  35499  rankfilimbi  35617  cvmopnlem  35865  cvmfolem  35866  cvmliftmolem2  35869  cvmlift2lem10  35899  satf00  35961  satffunlem2lem1  35991  satefvfmla0  36005  mrsubvrs  36109  wzel  36409  btwnconn1lem8  36682  btwnconn1lem9  36683  btwnconn1lem10  36684  btwnconn1lem11  36685  btwnconn1lem12  36686  finminlem  36945  nn0prpwlem  36949  fnessref  36984  refssfne  36985  fnemeet2  36994  consym1  37047  bj-finsumval0  38045  topdifinffinlem  38109  relowlssretop  38125  rdgeqoa  38132  fvineqsneu  38173  pibt2  38179  poimirlem28  38405  mblfinlem1  38414  mblfinlem3  38416  mblfinlem4  38417  ovoliunnfl  38419  mbfresfi  38423  mbfposadd  38424  itg2addnclem2  38429  itg2addnc  38431  ftc1anc  38458  frinfm  38493  fdc  38503  blssp  38514  sstotbnd  38533  isbnd2  38541  ssbnd  38546  prdstotbnd  38552  prdsbnd2  38553  ismtyres  38566  heibor1lem  38567  rrnequiv  38593  rngoisocnv  38739  crngohomfo  38764  pridlc3  38831  membpartlem19  39670  prter3  39763  ax12eq  39822  ax12el  39823  cvratlem  40302  islvol2aN  40473  4atlem4b  40481  4atlem4c  40482  4atlem4d  40483  isline2  40655  isline3  40657  pclfinclN  40831  linepsubclN  40832  pexmidlem4N  40854  diaglbN  41936  dvhvaddcl  41976  dvhvaddcomN  41977  dvhvscacl  41984  djavalN  42016  dibglbN  42047  dihatexv  42219  djhval  42279  mapdrvallem2  42526  evlselvlem  43442  evlselv  43443  mhpind  43448  prjsprellsp  43465  elrfi  43547  nacsfix  43565  eldioph2  43615  lzenom  43623  rexrabdioph  43643  irrapxlem3  43673  pellexlem5  43682  pellex  43684  pell1234qrne0  43702  pell1234qrmulcl  43704  pell14qrdich  43718  pell1qrge1  43719  pellqrex  43728  rmxypairf1o  43760  rmxycomplete  43766  monotoddzzfi  43791  congadd  43815  jm2.19lem3  43840  jm2.19lem4  43841  jm2.25  43848  jm2.26a  43849  jm2.26lem3  43850  expdiophlem1  43870  wepwsolem  43891  lmhmfgsplit  43935  aaitgo  44011  mon1psubm  44048  deg1mhm  44049  succlg  44177  ofoacom  44210  iunrelexp0  44550  isotone2  44897  mnuprdlem4  45107  relpmin  45783  disjrnmpt2  46028  mullimc  46454  mullimcf  46461  climxrre  46586  fprodcncf  46736  stoweidlem17  46853  stoweidlem27  46863  stoweidlem54  46890  fourierdlem42  46985  fourierdlem62  47004  fourierdlem73  47015  fourierdlem76  47018  fourierdlem97  47039  sge0iunmptlemfi  47249  isomenndlem  47366  imarnf1pr  48178  smonoord  48273  fvelsetpreimafv  48295  iccpartiltu  48330  sprsymrelf1lem  48399  prproropf1olem3  48413  paireqne  48419  fmtnoprmfac1  48476  prmdvdsfmtnof1lem2  48496  nprmdvdsfacm1  48535  gricushgr  48841  grimedg  48859  cycl3grtri  48871  gpgedg2iv  48991  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  rngcinvALTV  49199  funcringcsetcALTV2lem9  49221  ringcinvALTV  49233  funcringcsetclem9ALTV  49244  lmodvsmdi  49317  lincsum  49367  lindslinindimp2lem4  49399  nn0sumshdiglemB  49558  1arymaptf1  49580  2arymaptf1  49591  dmrnxp  49773  xpco2  49793  initopropd  50177  termopropd  50178  zeroopropd  50179  oduoppcciso  50500  lanpropd  50549  ranpropd  50550