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  4803  prproe  4854  fr2nr  5591  wereu2  5611  f1oprg  6808  fvtp1g  7132  funfvima3  7170  isof1oidb  7258  isomin  7271  weniso  7288  elovmpt3rab1  7606  sorpssi  7662  resf1extb  7864  poseq  8088  suppofssd  8133  tfrlem9a  8305  oalimcl  8475  odi  8494  oeeui  8517  ralxpmap  8820  boxriin  8864  domdifsn  8973  domunsncan  8990  enfixsn  8999  disjen  9047  mapen  9054  mapxpen  9056  mapunen  9059  findcard2d  9076  unxpdomlem2  9141  unxpdomlem3  9142  isfinite2  9182  marypha1lem  9317  marypha2  9323  supmo  9336  infmo  9381  card2inf  9441  brwdom2  9459  wemapwe  9587  rankonidlem  9721  rankxplim3  9774  djulf1o  9805  djurf1o  9806  infxpenlem  9904  infxpenc2lem1  9910  infxpenc2  9913  fseqenlem1  9915  fseqenlem2  9916  infpwfien  9953  dfac12lem2  10036  infunsdom1  10103  infunsdom  10104  infmap2  10108  fin2i2  10209  fin23lem28  10231  fin23lem32  10235  fin23lem34  10237  fin23lem40  10242  isf32lem2  10245  compssiso  10265  isfin1-3  10277  fin1a2lem10  10300  fin12  10304  hsmexlem4  10320  ac6num  10370  ttukeylem7  10406  axdclem2  10411  iundom2g  10431  fpwwe2lem11  10532  pwfseqlem3  10551  winalim2  10587  winafp  10588  wunex2  10629  grur1  10711  dedekindle  11277  00id  11288  receu  11762  lt2mul2div  12000  peano5uzi  12562  uzwo  12809  qbtwnre  13098  iooshf  13326  modmul1  13831  seqcl2  13927  seqfveq2  13931  seqid2  13955  seqdistr  13960  expcl2lem  13980  mulexpz  14009  expnlbnd2  14141  hashfun  14344  hashfacen  14361  hashf1lem1  14362  elss2prb  14395  fstwrdne0  14463  swrdsb0eq  14571  swrdswrd  14612  wrd2ind  14630  swrdccatin1  14632  pfxccatin12  14640  splid  14660  repswrevw  14694  cshwidxmod  14710  cshwidx0  14713  2cshw  14720  cshweqrep  14728  cshw1  14729  wwlktovfo  14865  relexpfld  14956  relexpindlem  14970  01sqrexlem6  15154  absexpz  15212  o1rlimmul  15526  iseralt  15592  summolem2  15623  fsumf1o  15630  fsum0diag2  15690  fsummulc2  15691  cvgcmpce  15725  incexclem  15743  prodmolem2  15842  fprodcl2lem  15857  fprodmul  15867  fprodrev  15884  moddvds  16174  dvdsflip  16228  bitsf1ocnv  16355  sadcaddlem  16368  bezoutlem2  16451  bezoutlem4  16453  dfgcd2  16457  lcmgcdlem  16517  crth  16689  hashgcdlem  16699  phisum  16702  pcqcl  16768  pcid  16785  pcneg  16786  prmpwdvds  16816  pockthg  16818  4sqlem11  16867  ramub2  16926  0ram  16932  prmgaplem7  16969  prmgaplem8  16970  setscom  17091  qusval  17446  initoeu1  17918  termoeu1  17925  setcinv  17997  funcestrcsetclem9  18054  funcsetcestrclem9  18069  fullsetcestrc  18072  1stfcl  18103  2ndfcl  18104  hofpropd  18173  isacs3lem  18448  mgmhmlin  18607  mndpsuppss  18673  frmdss2  18771  frmdup1  18772  mgm2nsgrplem2  18827  mulgdirlem  19018  mulgass  19024  0nsg  19081  cycsubgcl  19118  ghmmulg  19140  conjghm  19161  qusghm  19167  gsumwrev  19278  symg2bas  19305  symgfixelsi  19347  f1otrspeq  19359  psgnunilem2  19407  psgnunilem3  19408  odf1o2  19485  lsmhash  19617  efgtf  19634  efginvrel2  19639  efgredeu  19664  efgcpbllemb  19667  frgpuplem  19684  frgpup1  19687  ghmcyg  19808  gsumval3lem1  19817  gsumzres  19821  gsumzcl2  19822  gsumzf1o  19824  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  gsumzoppg  19856  gsum2d  19884  subgdmdprd  19948  pgpfac1lem3  19991  gsummgp0  20236  rnghmmul  20367  rngcinv  20552  ringcinv  20586  islmodd  20799  lmodvsmmulgdi  20830  islss3  20892  0lmhm  20974  idlmhm  20975  lmhmeql  20989  pwssplit3  20995  lidldvgen  21271  qsssubdrg  21363  cnsubrg  21364  znf1o  21488  psgnghm  21517  psgndif  21539  cssmre  21630  dsmmsubg  21680  frlmup1  21735  lindfrn  21758  f1lindf  21759  evlslem1  22017  psdmul  22081  coe1tmmul2  22190  pf1ind  22270  mamufval  22307  mamurid  22357  mvmulfval  22457  mdetralt2  22524  mndifsplit  22551  maducoeval2  22555  madugsum  22558  mat2pmatmul  22646  decpmatmul  22687  pm2mpf1lem  22709  pm2mpf1  22714  monmat2matmon  22739  chpscmat  22757  fvmptnn04if  22764  tgcl  22884  ppttop  22922  epttop  22924  clsval2  22965  opncldf1  22999  mretopd  23007  neindisj  23032  neiptopnei  23047  restcls  23096  restntr  23097  ordtbas  23107  cnpnei  23179  cncls2  23188  tgcmp  23316  cmpcld  23317  uncmp  23318  hauscmplem  23321  1stcfb  23360  2ndcctbss  23370  hauspwdom  23416  reftr  23429  comppfsc  23447  kgentopon  23453  ptpjpre1  23486  ptcnplem  23536  txcn  23541  txdis1cn  23550  txhaus  23562  xkopt  23570  imasnopn  23605  imasncld  23606  imasncls  23607  hmeoimaf1o  23685  cmphaushmeo  23715  txhmeo  23718  trfbas2  23758  fbasfip  23783  fbasrn  23799  fmss  23861  elfm2  23863  hauspwpwf1  23902  flfcnp  23919  fclscf  23940  flimfnfcls  23943  fcfval  23948  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  ptcmplem3  23969  ptcmplem4  23970  cnextfval  23977  cnextcn  23982  tmdgsum2  24011  ustex2sym  24132  neipcfilu  24210  imasdsf1olem  24288  metss2lem  24426  stdbdxmet  24430  stdbdmopn  24433  metrest  24439  metcnp  24456  restmetu  24485  tngngp  24569  icccmplem1  24738  icccvx  24875  evth  24885  lebnumlem1  24887  pi1blem  24966  isncvsngp  25076  equivcau  25227  bcthlem5  25255  cmslssbn  25299  ivthlem3  25381  ovolicc2lem3  25447  ovolicc2lem4  25448  dyaddisj  25524  dyadmbllem  25527  ismbfd  25567  itg2seq  25670  itgss  25740  limciun  25822  dvcobr  25876  dvcobrOLD  25877  dvmptfsum  25906  c1liplem1  25928  c1lip1  25929  lhop  25948  dvcvx  25952  tdeglem4  25992  plyco0  26124  elply2  26128  plypf1  26144  dgreq0  26198  elqaalem2  26255  aalioulem6  26272  aaliou  26273  aaliou2b  26276  ulmss  26333  ulmcn  26335  pserulm  26358  lgamgulmlem5  26970  basellem4  27021  fsumdvdsdiaglem  27120  mpodvdsmulf1o  27131  dvdsmulf1o  27133  chtublem  27149  fsumvma2  27152  logfaclbnd  27160  dchrelbasd  27177  lgsqrlem2  27285  gausslemma2dlem1a  27303  lgseisenlem2  27314  lgsquadlem1  27318  lgsquadlem2  27319  lgsquadlem3  27320  rplogsumlem2  27423  rpvmasumlem  27425  dchrmusum2  27432  dchrvmasumlem1  27433  dchrvmasum2lem  27434  rpvmasum2  27450  dchrisum0lem1  27454  logsqvma  27480  selberg4  27499  pntibndlem3  27530  pntlem3  27547  ostthlem1  27565  ostthlem2  27566  sltres  27601  nogt01o  27635  oldbdayim  27834  addsproplem2  27913  negsproplem2  27971  mulsval  28048  om2noseqrdg  28234  noseqrdgfn  28236  zmulscld  28321  recut  28398  idmot  28515  brcgr  28878  brbtwn2  28883  axsegconlem8  28902  axpaschlem  28918  axeuclid  28941  axcontlem2  28943  axcontlem7  28948  eengtrkg  28964  upgrex  29070  subgrprop3  29254  subupgr  29265  nbgr0edglem  29334  nb3grprlem1  29358  cusgredg  29402  cusgrres  29427  usgredgsscusgredg  29438  finsumvtxdg2ssteplem4  29527  finsumvtxdg2sstep  29528  wlkl1loop  29616  wlkp1lem4  29653  wwlksnred  29870  wwlksnext  29871  wwlksnextwrd  29875  wpthswwlks2on  29942  clwwlknp  30017  clwwlkel  30026  wwlksext2clwwlk  30037  clwwlknonwwlknonb  30086  3wlkond  30151  1conngr  30174  eucrctshift  30223  fusgr2wsp2nb  30314  numclwwlk1lem2foa  30334  numclwwlk1lem2f1  30337  numclwlk1lem1  30349  numclwlk1lem2  30350  grpoidinvlem1  30484  grporcan  30498  ipblnfi  30835  hvmulcan2  31053  shscli  31297  spansneleq  31550  pjspansn  31557  3oalem2  31643  eigposi  31816  cnlnadjlem2  32048  stlesi  32221  mdslmd1lem1  32305  mdslmd1lem2  32306  cdj1i  32413  disjxpin  32568  nn0xmulclb  32754  xreceu  32902  txomap  33847  pstmxmet  33910  qqhghm  34001  qqhrhm  34002  measinblem  34233  cntmeas  34239  ballotlemsf1o  34527  bnj945  34785  bnj1110  34994  f1resveqaeq  35097  rankfilimbi  35112  cvmopnlem  35322  cvmfolem  35323  cvmliftmolem2  35326  cvmlift2lem10  35356  satf00  35418  satffunlem2lem1  35448  satefvfmla0  35462  mrsubvrs  35566  wzel  35866  btwnconn1lem8  36138  btwnconn1lem9  36139  btwnconn1lem10  36140  btwnconn1lem11  36141  btwnconn1lem12  36142  finminlem  36362  nn0prpwlem  36366  fnessref  36401  refssfne  36402  fnemeet2  36411  consym1  36464  bj-finsumval0  37329  topdifinffinlem  37391  relowlssretop  37407  rdgeqoa  37414  fvineqsneu  37455  pibt2  37461  matunitlindflem1  37666  poimirlem28  37698  mblfinlem1  37707  mblfinlem3  37709  mblfinlem4  37710  ovoliunnfl  37712  mbfresfi  37716  mbfposadd  37717  itg2addnclem2  37722  itg2addnc  37724  ftc1anc  37751  frinfm  37785  fdc  37795  blssp  37806  sstotbnd  37825  isbnd2  37833  ssbnd  37838  prdstotbnd  37844  prdsbnd2  37845  ismtyres  37858  heibor1lem  37859  rrnequiv  37885  rngoisocnv  38031  crngohomfo  38056  pridlc3  38123  membpartlem19  38919  prter3  38991  ax12eq  39050  ax12el  39051  cvratlem  39530  islvol2aN  39701  4atlem4b  39709  4atlem4c  39710  4atlem4d  39711  isline2  39883  isline3  39885  pclfinclN  40059  linepsubclN  40060  pexmidlem4N  40082  diaglbN  41164  dvhvaddcl  41204  dvhvaddcomN  41205  dvhvscacl  41212  djavalN  41244  dibglbN  41275  dihatexv  41447  djhval  41507  mapdrvallem2  41754  evlselvlem  42689  evlselv  42690  mhpind  42697  prjsprellsp  42714  elrfi  42797  nacsfix  42815  eldioph2  42865  lzenom  42873  rexrabdioph  42897  irrapxlem3  42927  pellexlem5  42936  pellex  42938  pell1234qrne0  42956  pell1234qrmulcl  42958  pell14qrdich  42972  pell1qrge1  42973  pellqrex  42982  rmxypairf1o  43014  rmxycomplete  43020  monotoddzzfi  43045  congadd  43069  jm2.19lem3  43094  jm2.19lem4  43095  jm2.25  43102  jm2.26a  43103  jm2.26lem3  43104  expdiophlem1  43124  wepwsolem  43145  lmhmfgsplit  43189  aaitgo  43265  mon1psubm  43302  deg1mhm  43303  succlg  43431  ofoacom  43464  iunrelexp0  43805  isotone2  44152  mnuprdlem4  44378  relpmin  45055  disjrnmpt2  45295  mullimc  45726  mullimcf  45733  climxrre  45858  fprodcncf  46008  stoweidlem17  46125  stoweidlem27  46135  stoweidlem54  46162  fourierdlem42  46257  fourierdlem62  46276  fourierdlem73  46287  fourierdlem76  46290  fourierdlem97  46311  sge0iunmptlemfi  46521  isomenndlem  46638  imarnf1pr  47392  smonoord  47481  fvelsetpreimafv  47497  iccpartiltu  47532  sprsymrelf1lem  47601  prproropf1olem3  47615  paireqne  47621  fmtnoprmfac1  47675  prmdvdsfmtnof1lem2  47695  gricushgr  48027  grimedg  48045  cycl3grtri  48057  gpgedg2iv  48177  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  rngcinvALTV  48386  funcringcsetcALTV2lem9  48408  ringcinvALTV  48420  funcringcsetclem9ALTV  48431  lmodvsmdi  48489  lincsum  48540  lindslinindimp2lem4  48572  nn0sumshdiglemB  48731  1arymaptf1  48753  2arymaptf1  48764  dmrnxp  48947  xpco2  48967  initopropd  49354  termopropd  49355  zeroopropd  49356  oduoppcciso  49677  lanpropd  49726  ranpropd  49727