Theorem ad2antll 730

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  773  simprrl  781  simprrr  782  simprr1  1223  simprr2  1224  simprr3  1225  prneimg  4798  prproe  4849  fr2nr  5602  wereu2  5622  f1oprg  6821  fvtp1g  7147  funfvima3  7185  isof1oidb  7273  isomin  7286  weniso  7303  elovmpt3rab1  7621  sorpssi  7677  resf1extb  7879  poseq  8102  suppofssd  8147  tfrlem9a  8319  oalimcl  8489  odi  8508  oeeui  8532  ralxpmap  8838  boxriin  8882  domdifsn  8992  domunsncan  9009  enfixsn  9018  disjen  9066  mapen  9073  mapxpen  9075  mapunen  9078  findcard2d  9095  unxpdomlem2  9161  unxpdomlem3  9162  isfinite2  9202  marypha1lem  9340  marypha2  9346  supmo  9359  infmo  9404  card2inf  9464  brwdom2  9482  wemapwe  9612  rankonidlem  9746  rankxplim3  9799  djulf1o  9830  djurf1o  9831  infxpenlem  9929  infxpenc2lem1  9935  infxpenc2  9938  fseqenlem1  9940  fseqenlem2  9941  infpwfien  9978  dfac12lem2  10061  infunsdom1  10128  infunsdom  10129  infmap2  10133  fin2i2  10234  fin23lem28  10256  fin23lem32  10260  fin23lem34  10262  fin23lem40  10267  isf32lem2  10270  compssiso  10290  isfin1-3  10302  fin1a2lem10  10325  fin12  10329  hsmexlem4  10345  ac6num  10395  ttukeylem7  10431  axdclem2  10436  iundom2g  10456  fpwwe2lem11  10558  pwfseqlem3  10577  winalim2  10613  winafp  10614  wunex2  10655  grur1  10737  dedekindle  11304  00id  11315  receu  11789  lt2mul2div  12028  peano5uzi  12612  uzwo  12855  qbtwnre  13145  iooshf  13373  modmul1  13880  seqcl2  13976  seqfveq2  13980  seqid2  14004  seqdistr  14009  expcl2lem  14029  mulexpz  14058  expnlbnd2  14190  hashfun  14393  hashfacen  14410  hashf1lem1  14411  elss2prb  14444  fstwrdne0  14512  swrdsb0eq  14620  swrdswrd  14661  wrd2ind  14679  swrdccatin1  14681  pfxccatin12  14689  splid  14709  repswrevw  14743  cshwidxmod  14759  cshwidx0  14762  2cshw  14769  cshweqrep  14777  cshw1  14778  wwlktovfo  14914  relexpfld  15005  relexpindlem  15019  01sqrexlem6  15203  absexpz  15261  o1rlimmul  15575  iseralt  15641  summolem2  15672  fsumf1o  15679  fsum0diag2  15739  fsummulc2  15740  cvgcmpce  15775  incexclem  15795  prodmolem2  15894  fprodcl2lem  15909  fprodmul  15919  fprodrev  15936  moddvds  16226  dvdsflip  16280  bitsf1ocnv  16407  sadcaddlem  16420  bezoutlem2  16503  bezoutlem4  16505  dfgcd2  16509  lcmgcdlem  16569  crth  16742  hashgcdlem  16752  phisum  16755  pcqcl  16821  pcid  16838  pcneg  16839  prmpwdvds  16869  pockthg  16871  4sqlem11  16920  ramub2  16979  0ram  16985  prmgaplem7  17022  prmgaplem8  17023  setscom  17144  qusval  17500  initoeu1  17972  termoeu1  17979  setcinv  18051  funcestrcsetclem9  18108  funcsetcestrclem9  18123  fullsetcestrc  18126  1stfcl  18157  2ndfcl  18158  hofpropd  18227  isacs3lem  18502  mgmhmlin  18661  mndpsuppss  18727  frmdss2  18825  frmdup1  18826  mgm2nsgrplem2  18884  mulgdirlem  19075  mulgass  19081  0nsg  19138  cycsubgcl  19175  ghmmulg  19197  conjghm  19218  qusghm  19224  gsumwrev  19335  symg2bas  19362  symgfixelsi  19404  f1otrspeq  19416  psgnunilem2  19464  psgnunilem3  19465  odf1o2  19542  lsmhash  19674  efgtf  19691  efginvrel2  19696  efgredeu  19721  efgcpbllemb  19724  frgpuplem  19741  frgpup1  19744  ghmcyg  19865  gsumval3lem1  19874  gsumzres  19878  gsumzcl2  19879  gsumzf1o  19881  gsumzaddlem  19890  gsumconst  19903  gsumzmhm  19906  gsumzoppg  19913  gsum2d  19941  subgdmdprd  20005  pgpfac1lem3  20048  gsummgp0  20291  rnghmmul  20423  rngcinv  20608  ringcinv  20642  islmodd  20855  lmodvsmmulgdi  20886  islss3  20948  0lmhm  21030  idlmhm  21031  lmhmeql  21045  pwssplit3  21051  lidldvgen  21327  qsssubdrg  21419  cnsubrg  21420  znf1o  21544  psgnghm  21573  psgndif  21595  cssmre  21686  dsmmsubg  21736  frlmup1  21791  lindfrn  21814  f1lindf  21815  evlslem1  22073  psdmul  22145  coe1tmmul2  22254  pf1ind  22333  mamufval  22370  mamurid  22420  mvmulfval  22520  mdetralt2  22587  mndifsplit  22614  maducoeval2  22618  madugsum  22621  mat2pmatmul  22709  decpmatmul  22750  pm2mpf1lem  22772  pm2mpf1  22777  monmat2matmon  22802  chpscmat  22820  fvmptnn04if  22827  tgcl  22947  ppttop  22985  epttop  22987  clsval2  23028  opncldf1  23062  mretopd  23070  neindisj  23095  neiptopnei  23110  restcls  23159  restntr  23160  ordtbas  23170  cnpnei  23242  cncls2  23251  tgcmp  23379  cmpcld  23380  uncmp  23381  hauscmplem  23384  1stcfb  23423  2ndcctbss  23433  hauspwdom  23479  reftr  23492  comppfsc  23510  kgentopon  23516  ptpjpre1  23549  ptcnplem  23599  txcn  23604  txdis1cn  23613  txhaus  23625  xkopt  23633  imasnopn  23668  imasncld  23669  imasncls  23670  hmeoimaf1o  23748  cmphaushmeo  23778  txhmeo  23781  trfbas2  23821  fbasfip  23846  fbasrn  23862  fmss  23924  elfm2  23926  hauspwpwf1  23965  flfcnp  23982  fclscf  24003  flimfnfcls  24006  fcfval  24011  alexsubALTlem2  24026  alexsubALTlem3  24027  alexsubALTlem4  24028  ptcmplem3  24032  ptcmplem4  24033  cnextfval  24040  cnextcn  24045  tmdgsum2  24074  ustex2sym  24195  neipcfilu  24273  imasdsf1olem  24351  metss2lem  24489  stdbdxmet  24493  stdbdmopn  24496  metrest  24502  metcnp  24519  restmetu  24548  tngngp  24632  icccmplem1  24801  icccvx  24930  evth  24939  lebnumlem1  24941  pi1blem  25019  isncvsngp  25129  equivcau  25280  bcthlem5  25308  cmslssbn  25352  ivthlem3  25433  ovolicc2lem3  25499  ovolicc2lem4  25500  dyaddisj  25576  dyadmbllem  25579  ismbfd  25619  itg2seq  25722  itgss  25792  limciun  25874  dvcobr  25926  dvmptfsum  25955  c1liplem1  25976  c1lip1  25977  lhop  25996  dvcvx  26000  tdeglem4  26038  plyco0  26170  elply2  26174  plypf1  26190  dgreq0  26243  elqaalem2  26300  aalioulem6  26317  aaliou  26318  aaliou2b  26321  ulmss  26378  ulmcn  26380  pserulm  26403  lgamgulmlem5  27013  basellem4  27064  fsumdvdsdiaglem  27163  mpodvdsmulf1o  27174  dvdsmulf1o  27176  chtublem  27191  fsumvma2  27194  logfaclbnd  27202  dchrelbasd  27219  lgsqrlem2  27327  gausslemma2dlem1a  27345  lgseisenlem2  27356  lgsquadlem1  27360  lgsquadlem2  27361  lgsquadlem3  27362  rplogsumlem2  27465  rpvmasumlem  27467  dchrmusum2  27474  dchrvmasumlem1  27475  dchrvmasum2lem  27476  rpvmasum2  27492  dchrisum0lem1  27496  logsqvma  27522  selberg4  27541  pntibndlem3  27572  pntlem3  27589  ostthlem1  27607  ostthlem2  27608  ltsres  27643  nogt01o  27677  oldbdayim  27898  addsproplem2  27979  negsproplem2  28038  mulsval  28118  om2noseqrdg  28313  noseqrdgfn  28315  zmulscld  28406  recut  28503  idmot  28622  brcgr  28986  brbtwn2  28991  axsegconlem8  29010  axpaschlem  29026  axeuclid  29049  axcontlem2  29051  axcontlem7  29056  eengtrkg  29072  upgrex  29178  subgrprop3  29362  subupgr  29373  nbgr0edglem  29442  nb3grprlem1  29466  cusgredg  29510  cusgrres  29535  usgredgsscusgredg  29546  finsumvtxdg2ssteplem4  29635  finsumvtxdg2sstep  29636  wlkl1loop  29724  wlkp1lem4  29761  wwlksnred  29978  wwlksnext  29979  wwlksnextwrd  29983  wpthswwlks2on  30050  clwwlknp  30125  clwwlkel  30134  wwlksext2clwwlk  30145  clwwlknonwwlknonb  30194  3wlkond  30259  1conngr  30282  eucrctshift  30331  fusgr2wsp2nb  30422  numclwwlk1lem2foa  30442  numclwwlk1lem2f1  30445  numclwlk1lem1  30457  numclwlk1lem2  30458  grpoidinvlem1  30593  grporcan  30607  ipblnfi  30944  hvmulcan2  31162  shscli  31406  spansneleq  31659  pjspansn  31666  3oalem2  31752  eigposi  31925  cnlnadjlem2  32157  stlesi  32330  mdslmd1lem1  32414  mdslmd1lem2  32415  cdj1i  32522  disjxpin  32676  nn0xmulclb  32862  xreceu  32999  txomap  33997  pstmxmet  34060  qqhghm  34151  qqhrhm  34152  measinblem  34383  cntmeas  34389  ballotlemsf1o  34677  bnj945  34935  bnj1110  35143  f1resveqaeq  35247  rankfilimbi  35263  cvmopnlem  35479  cvmfolem  35480  cvmliftmolem2  35483  cvmlift2lem10  35513  satf00  35575  satffunlem2lem1  35605  satefvfmla0  35619  mrsubvrs  35723  wzel  36023  btwnconn1lem8  36295  btwnconn1lem9  36296  btwnconn1lem10  36297  btwnconn1lem11  36298  btwnconn1lem12  36299  finminlem  36519  nn0prpwlem  36523  fnessref  36558  refssfne  36559  fnemeet2  36568  consym1  36621  bj-finsumval0  37618  topdifinffinlem  37680  relowlssretop  37696  rdgeqoa  37703  fvineqsneu  37744  pibt2  37750  matunitlindflem1  37954  poimirlem28  37986  mblfinlem1  37995  mblfinlem3  37997  mblfinlem4  37998  ovoliunnfl  38000  mbfresfi  38004  mbfposadd  38005  itg2addnclem2  38010  itg2addnc  38012  ftc1anc  38039  frinfm  38073  fdc  38083  blssp  38094  sstotbnd  38113  isbnd2  38121  ssbnd  38126  prdstotbnd  38132  prdsbnd2  38133  ismtyres  38146  heibor1lem  38147  rrnequiv  38173  rngoisocnv  38319  crngohomfo  38344  pridlc3  38411  membpartlem19  39252  prter3  39345  ax12eq  39404  ax12el  39405  cvratlem  39884  islvol2aN  40055  4atlem4b  40063  4atlem4c  40064  4atlem4d  40065  isline2  40237  isline3  40239  pclfinclN  40413  linepsubclN  40414  pexmidlem4N  40436  diaglbN  41518  dvhvaddcl  41558  dvhvaddcomN  41559  dvhvscacl  41566  djavalN  41598  dibglbN  41629  dihatexv  41801  djhval  41861  mapdrvallem2  42108  evlselvlem  43036  evlselv  43037  mhpind  43044  prjsprellsp  43061  elrfi  43143  nacsfix  43161  eldioph2  43211  lzenom  43219  rexrabdioph  43243  irrapxlem3  43273  pellexlem5  43282  pellex  43284  pell1234qrne0  43302  pell1234qrmulcl  43304  pell14qrdich  43318  pell1qrge1  43319  pellqrex  43328  rmxypairf1o  43360  rmxycomplete  43366  monotoddzzfi  43391  congadd  43415  jm2.19lem3  43440  jm2.19lem4  43441  jm2.25  43448  jm2.26a  43449  jm2.26lem3  43450  expdiophlem1  43470  wepwsolem  43491  lmhmfgsplit  43535  aaitgo  43611  mon1psubm  43648  deg1mhm  43649  succlg  43777  ofoacom  43810  iunrelexp0  44150  isotone2  44497  mnuprdlem4  44723  relpmin  45400  disjrnmpt2  45639  mullimc  46067  mullimcf  46074  climxrre  46199  fprodcncf  46349  stoweidlem17  46466  stoweidlem27  46476  stoweidlem54  46503  fourierdlem42  46598  fourierdlem62  46617  fourierdlem73  46628  fourierdlem76  46631  fourierdlem97  46652  sge0iunmptlemfi  46862  isomenndlem  46979  imarnf1pr  47745  smonoord  47840  fvelsetpreimafv  47862  iccpartiltu  47897  sprsymrelf1lem  47966  prproropf1olem3  47980  paireqne  47986  fmtnoprmfac1  48043  prmdvdsfmtnof1lem2  48063  nprmdvdsfacm1  48102  gricushgr  48408  grimedg  48426  cycl3grtri  48438  gpgedg2iv  48558  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  rngcinvALTV  48767  funcringcsetcALTV2lem9  48789  ringcinvALTV  48801  funcringcsetclem9ALTV  48812  lmodvsmdi  48870  lincsum  48920  lindslinindimp2lem4  48952  nn0sumshdiglemB  49111  1arymaptf1  49133  2arymaptf1  49144  dmrnxp  49327  xpco2  49347  initopropd  49733  termopropd  49734  zeroopropd  49735  oduoppcciso  50056  lanpropd  50105  ranpropd  50106