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  4808  prproe  4859  fr2nr  5599  wereu2  5619  f1oprg  6818  fvtp1g  7142  funfvima3  7180  isof1oidb  7268  isomin  7281  weniso  7298  elovmpt3rab1  7616  sorpssi  7672  resf1extb  7874  poseq  8098  suppofssd  8143  tfrlem9a  8315  oalimcl  8485  odi  8504  oeeui  8528  ralxpmap  8832  boxriin  8876  domdifsn  8986  domunsncan  9003  enfixsn  9012  disjen  9060  mapen  9067  mapxpen  9069  mapunen  9072  findcard2d  9089  unxpdomlem2  9155  unxpdomlem3  9156  isfinite2  9196  marypha1lem  9334  marypha2  9340  supmo  9353  infmo  9398  card2inf  9458  brwdom2  9476  wemapwe  9604  rankonidlem  9738  rankxplim3  9791  djulf1o  9822  djurf1o  9823  infxpenlem  9921  infxpenc2lem1  9927  infxpenc2  9930  fseqenlem1  9932  fseqenlem2  9933  infpwfien  9970  dfac12lem2  10053  infunsdom1  10120  infunsdom  10121  infmap2  10125  fin2i2  10226  fin23lem28  10248  fin23lem32  10252  fin23lem34  10254  fin23lem40  10259  isf32lem2  10262  compssiso  10282  isfin1-3  10294  fin1a2lem10  10317  fin12  10321  hsmexlem4  10337  ac6num  10387  ttukeylem7  10423  axdclem2  10428  iundom2g  10448  fpwwe2lem11  10550  pwfseqlem3  10569  winalim2  10605  winafp  10606  wunex2  10647  grur1  10729  dedekindle  11295  00id  11306  receu  11780  lt2mul2div  12018  peano5uzi  12579  uzwo  12822  qbtwnre  13112  iooshf  13340  modmul1  13845  seqcl2  13941  seqfveq2  13945  seqid2  13969  seqdistr  13974  expcl2lem  13994  mulexpz  14023  expnlbnd2  14155  hashfun  14358  hashfacen  14375  hashf1lem1  14376  elss2prb  14409  fstwrdne0  14477  swrdsb0eq  14585  swrdswrd  14626  wrd2ind  14644  swrdccatin1  14646  pfxccatin12  14654  splid  14674  repswrevw  14708  cshwidxmod  14724  cshwidx0  14727  2cshw  14734  cshweqrep  14742  cshw1  14743  wwlktovfo  14879  relexpfld  14970  relexpindlem  14984  01sqrexlem6  15168  absexpz  15226  o1rlimmul  15540  iseralt  15606  summolem2  15637  fsumf1o  15644  fsum0diag2  15704  fsummulc2  15705  cvgcmpce  15739  incexclem  15757  prodmolem2  15856  fprodcl2lem  15871  fprodmul  15881  fprodrev  15898  moddvds  16188  dvdsflip  16242  bitsf1ocnv  16369  sadcaddlem  16382  bezoutlem2  16465  bezoutlem4  16467  dfgcd2  16471  lcmgcdlem  16531  crth  16703  hashgcdlem  16713  phisum  16716  pcqcl  16782  pcid  16799  pcneg  16800  prmpwdvds  16830  pockthg  16832  4sqlem11  16881  ramub2  16940  0ram  16946  prmgaplem7  16983  prmgaplem8  16984  setscom  17105  qusval  17461  initoeu1  17933  termoeu1  17940  setcinv  18012  funcestrcsetclem9  18069  funcsetcestrclem9  18084  fullsetcestrc  18087  1stfcl  18118  2ndfcl  18119  hofpropd  18188  isacs3lem  18463  mgmhmlin  18622  mndpsuppss  18688  frmdss2  18786  frmdup1  18787  mgm2nsgrplem2  18842  mulgdirlem  19033  mulgass  19039  0nsg  19096  cycsubgcl  19133  ghmmulg  19155  conjghm  19176  qusghm  19182  gsumwrev  19293  symg2bas  19320  symgfixelsi  19362  f1otrspeq  19374  psgnunilem2  19422  psgnunilem3  19423  odf1o2  19500  lsmhash  19632  efgtf  19649  efginvrel2  19654  efgredeu  19679  efgcpbllemb  19682  frgpuplem  19699  frgpup1  19702  ghmcyg  19823  gsumval3lem1  19832  gsumzres  19836  gsumzcl2  19837  gsumzf1o  19839  gsumzaddlem  19848  gsumconst  19861  gsumzmhm  19864  gsumzoppg  19871  gsum2d  19899  subgdmdprd  19963  pgpfac1lem3  20006  gsummgp0  20251  rnghmmul  20383  rngcinv  20568  ringcinv  20602  islmodd  20815  lmodvsmmulgdi  20846  islss3  20908  0lmhm  20990  idlmhm  20991  lmhmeql  21005  pwssplit3  21011  lidldvgen  21287  qsssubdrg  21379  cnsubrg  21380  znf1o  21504  psgnghm  21533  psgndif  21555  cssmre  21646  dsmmsubg  21696  frlmup1  21751  lindfrn  21774  f1lindf  21775  evlslem1  22035  psdmul  22107  coe1tmmul2  22216  pf1ind  22297  mamufval  22334  mamurid  22384  mvmulfval  22484  mdetralt2  22551  mndifsplit  22578  maducoeval2  22582  madugsum  22585  mat2pmatmul  22673  decpmatmul  22714  pm2mpf1lem  22736  pm2mpf1  22741  monmat2matmon  22766  chpscmat  22784  fvmptnn04if  22791  tgcl  22911  ppttop  22949  epttop  22951  clsval2  22992  opncldf1  23026  mretopd  23034  neindisj  23059  neiptopnei  23074  restcls  23123  restntr  23124  ordtbas  23134  cnpnei  23206  cncls2  23215  tgcmp  23343  cmpcld  23344  uncmp  23345  hauscmplem  23348  1stcfb  23387  2ndcctbss  23397  hauspwdom  23443  reftr  23456  comppfsc  23474  kgentopon  23480  ptpjpre1  23513  ptcnplem  23563  txcn  23568  txdis1cn  23577  txhaus  23589  xkopt  23597  imasnopn  23632  imasncld  23633  imasncls  23634  hmeoimaf1o  23712  cmphaushmeo  23742  txhmeo  23745  trfbas2  23785  fbasfip  23810  fbasrn  23826  fmss  23888  elfm2  23890  hauspwpwf1  23929  flfcnp  23946  fclscf  23967  flimfnfcls  23970  fcfval  23975  alexsubALTlem2  23990  alexsubALTlem3  23991  alexsubALTlem4  23992  ptcmplem3  23996  ptcmplem4  23997  cnextfval  24004  cnextcn  24009  tmdgsum2  24038  ustex2sym  24159  neipcfilu  24237  imasdsf1olem  24315  metss2lem  24453  stdbdxmet  24457  stdbdmopn  24460  metrest  24466  metcnp  24483  restmetu  24512  tngngp  24596  icccmplem1  24765  icccvx  24902  evth  24912  lebnumlem1  24914  pi1blem  24993  isncvsngp  25103  equivcau  25254  bcthlem5  25282  cmslssbn  25326  ivthlem3  25408  ovolicc2lem3  25474  ovolicc2lem4  25475  dyaddisj  25551  dyadmbllem  25554  ismbfd  25594  itg2seq  25697  itgss  25767  limciun  25849  dvcobr  25903  dvcobrOLD  25904  dvmptfsum  25933  c1liplem1  25955  c1lip1  25956  lhop  25975  dvcvx  25979  tdeglem4  26019  plyco0  26151  elply2  26155  plypf1  26171  dgreq0  26225  elqaalem2  26282  aalioulem6  26299  aaliou  26300  aaliou2b  26303  ulmss  26360  ulmcn  26362  pserulm  26385  lgamgulmlem5  26997  basellem4  27048  fsumdvdsdiaglem  27147  mpodvdsmulf1o  27158  dvdsmulf1o  27160  chtublem  27176  fsumvma2  27179  logfaclbnd  27187  dchrelbasd  27204  lgsqrlem2  27312  gausslemma2dlem1a  27330  lgseisenlem2  27341  lgsquadlem1  27345  lgsquadlem2  27346  lgsquadlem3  27347  rplogsumlem2  27450  rpvmasumlem  27452  dchrmusum2  27459  dchrvmasumlem1  27460  dchrvmasum2lem  27461  rpvmasum2  27477  dchrisum0lem1  27481  logsqvma  27507  selberg4  27526  pntibndlem3  27557  pntlem3  27574  ostthlem1  27592  ostthlem2  27593  sltres  27628  nogt01o  27662  oldbdayim  27861  addsproplem2  27940  negsproplem2  27998  mulsval  28078  om2noseqrdg  28265  noseqrdgfn  28267  zmulscld  28355  recut  28439  idmot  28558  brcgr  28922  brbtwn2  28927  axsegconlem8  28946  axpaschlem  28962  axeuclid  28985  axcontlem2  28987  axcontlem7  28992  eengtrkg  29008  upgrex  29114  subgrprop3  29298  subupgr  29309  nbgr0edglem  29378  nb3grprlem1  29402  cusgredg  29446  cusgrres  29471  usgredgsscusgredg  29482  finsumvtxdg2ssteplem4  29571  finsumvtxdg2sstep  29572  wlkl1loop  29660  wlkp1lem4  29697  wwlksnred  29914  wwlksnext  29915  wwlksnextwrd  29919  wpthswwlks2on  29986  clwwlknp  30061  clwwlkel  30070  wwlksext2clwwlk  30081  clwwlknonwwlknonb  30130  3wlkond  30195  1conngr  30218  eucrctshift  30267  fusgr2wsp2nb  30358  numclwwlk1lem2foa  30378  numclwwlk1lem2f1  30381  numclwlk1lem1  30393  numclwlk1lem2  30394  grpoidinvlem1  30528  grporcan  30542  ipblnfi  30879  hvmulcan2  31097  shscli  31341  spansneleq  31594  pjspansn  31601  3oalem2  31687  eigposi  31860  cnlnadjlem2  32092  stlesi  32265  mdslmd1lem1  32349  mdslmd1lem2  32350  cdj1i  32457  disjxpin  32612  nn0xmulclb  32800  xreceu  32952  txomap  33940  pstmxmet  34003  qqhghm  34094  qqhrhm  34095  measinblem  34326  cntmeas  34332  ballotlemsf1o  34620  bnj945  34878  bnj1110  35087  f1resveqaeq  35190  rankfilimbi  35206  cvmopnlem  35421  cvmfolem  35422  cvmliftmolem2  35425  cvmlift2lem10  35455  satf00  35517  satffunlem2lem1  35547  satefvfmla0  35561  mrsubvrs  35665  wzel  35965  btwnconn1lem8  36237  btwnconn1lem9  36238  btwnconn1lem10  36239  btwnconn1lem11  36240  btwnconn1lem12  36241  finminlem  36461  nn0prpwlem  36465  fnessref  36500  refssfne  36501  fnemeet2  36510  consym1  36563  bj-finsumval0  37429  topdifinffinlem  37491  relowlssretop  37507  rdgeqoa  37514  fvineqsneu  37555  pibt2  37561  matunitlindflem1  37756  poimirlem28  37788  mblfinlem1  37797  mblfinlem3  37799  mblfinlem4  37800  ovoliunnfl  37802  mbfresfi  37806  mbfposadd  37807  itg2addnclem2  37812  itg2addnc  37814  ftc1anc  37841  frinfm  37875  fdc  37885  blssp  37896  sstotbnd  37915  isbnd2  37923  ssbnd  37928  prdstotbnd  37934  prdsbnd2  37935  ismtyres  37948  heibor1lem  37949  rrnequiv  37975  rngoisocnv  38121  crngohomfo  38146  pridlc3  38213  membpartlem19  39009  prter3  39081  ax12eq  39140  ax12el  39141  cvratlem  39620  islvol2aN  39791  4atlem4b  39799  4atlem4c  39800  4atlem4d  39801  isline2  39973  isline3  39975  pclfinclN  40149  linepsubclN  40150  pexmidlem4N  40172  diaglbN  41254  dvhvaddcl  41294  dvhvaddcomN  41295  dvhvscacl  41302  djavalN  41334  dibglbN  41365  dihatexv  41537  djhval  41597  mapdrvallem2  41844  evlselvlem  42771  evlselv  42772  mhpind  42779  prjsprellsp  42796  elrfi  42878  nacsfix  42896  eldioph2  42946  lzenom  42954  rexrabdioph  42978  irrapxlem3  43008  pellexlem5  43017  pellex  43019  pell1234qrne0  43037  pell1234qrmulcl  43039  pell14qrdich  43053  pell1qrge1  43054  pellqrex  43063  rmxypairf1o  43095  rmxycomplete  43101  monotoddzzfi  43126  congadd  43150  jm2.19lem3  43175  jm2.19lem4  43176  jm2.25  43183  jm2.26a  43184  jm2.26lem3  43185  expdiophlem1  43205  wepwsolem  43226  lmhmfgsplit  43270  aaitgo  43346  mon1psubm  43383  deg1mhm  43384  succlg  43512  ofoacom  43545  iunrelexp0  43885  isotone2  44232  mnuprdlem4  44458  relpmin  45135  disjrnmpt2  45374  mullimc  45804  mullimcf  45811  climxrre  45936  fprodcncf  46086  stoweidlem17  46203  stoweidlem27  46213  stoweidlem54  46240  fourierdlem42  46335  fourierdlem62  46354  fourierdlem73  46365  fourierdlem76  46368  fourierdlem97  46389  sge0iunmptlemfi  46599  isomenndlem  46716  imarnf1pr  47470  smonoord  47559  fvelsetpreimafv  47575  iccpartiltu  47610  sprsymrelf1lem  47679  prproropf1olem3  47693  paireqne  47699  fmtnoprmfac1  47753  prmdvdsfmtnof1lem2  47773  gricushgr  48105  grimedg  48123  cycl3grtri  48135  gpgedg2iv  48255  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  rngcinvALTV  48464  funcringcsetcALTV2lem9  48486  ringcinvALTV  48498  funcringcsetclem9ALTV  48509  lmodvsmdi  48567  lincsum  48617  lindslinindimp2lem4  48649  nn0sumshdiglemB  48808  1arymaptf1  48830  2arymaptf1  48841  dmrnxp  49024  xpco2  49044  initopropd  49430  termopropd  49431  zeroopropd  49432  oduoppcciso  49753  lanpropd  49802  ranpropd  49803