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  4818  prproe  4869  fr2nr  5615  wereu2  5635  f1oprg  6845  fvtp1g  7172  funfvima3  7210  isof1oidb  7299  isomin  7312  weniso  7329  elovmpt3rab1  7649  sorpssi  7705  resf1extb  7910  poseq  8137  suppofssd  8182  tfrlem9a  8354  oalimcl  8524  odi  8543  oeeui  8566  ralxpmap  8869  boxriin  8913  domdifsn  9024  domunsncan  9041  enfixsn  9050  disjen  9098  mapen  9105  mapxpen  9107  mapunen  9110  findcard2d  9130  unxpdomlem2  9198  unxpdomlem3  9199  findcard3OLD  9230  isfinite2  9245  marypha1lem  9384  marypha2  9390  supmo  9403  infmo  9448  card2inf  9508  brwdom2  9526  wemapwe  9650  rankonidlem  9781  rankxplim3  9834  djulf1o  9865  djurf1o  9866  infxpenlem  9966  infxpenc2lem1  9972  infxpenc2  9975  fseqenlem1  9977  fseqenlem2  9978  infpwfien  10015  dfac12lem2  10098  infunsdom1  10165  infunsdom  10166  infmap2  10170  fin2i2  10271  fin23lem28  10293  fin23lem32  10297  fin23lem34  10299  fin23lem40  10304  isf32lem2  10307  compssiso  10327  isfin1-3  10339  fin1a2lem10  10362  fin12  10366  hsmexlem4  10382  ac6num  10432  ttukeylem7  10468  axdclem2  10473  iundom2g  10493  fpwwe2lem11  10594  pwfseqlem3  10613  winalim2  10649  winafp  10650  wunex2  10691  grur1  10773  dedekindle  11338  00id  11349  receu  11823  lt2mul2div  12061  peano5uzi  12623  uzwo  12870  qbtwnre  13159  iooshf  13387  modmul1  13889  seqcl2  13985  seqfveq2  13989  seqid2  14013  seqdistr  14018  expcl2lem  14038  mulexpz  14067  expnlbnd2  14199  hashfun  14402  hashfacen  14419  hashf1lem1  14420  elss2prb  14453  fstwrdne0  14521  swrdsb0eq  14628  swrdswrd  14670  wrd2ind  14688  swrdccatin1  14690  pfxccatin12  14698  splid  14718  repswrevw  14752  cshwidxmod  14768  cshwidx0  14771  2cshw  14778  cshweqrep  14786  cshw1  14787  wwlktovfo  14924  relexpfld  15015  relexpindlem  15029  01sqrexlem6  15213  absexpz  15271  o1rlimmul  15585  iseralt  15651  summolem2  15682  fsumf1o  15689  fsum0diag2  15749  fsummulc2  15750  cvgcmpce  15784  incexclem  15802  prodmolem2  15901  fprodcl2lem  15916  fprodmul  15926  fprodrev  15943  moddvds  16233  dvdsflip  16287  bitsf1ocnv  16414  sadcaddlem  16427  bezoutlem2  16510  bezoutlem4  16512  dfgcd2  16516  lcmgcdlem  16576  crth  16748  hashgcdlem  16758  phisum  16761  pcqcl  16827  pcid  16844  pcneg  16845  prmpwdvds  16875  pockthg  16877  4sqlem11  16926  ramub2  16985  0ram  16991  prmgaplem7  17028  prmgaplem8  17029  setscom  17150  qusval  17505  initoeu1  17973  termoeu1  17980  setcinv  18052  funcestrcsetclem9  18109  funcsetcestrclem9  18124  fullsetcestrc  18127  1stfcl  18158  2ndfcl  18159  hofpropd  18228  isacs3lem  18501  mgmhmlin  18626  mndpsuppss  18692  frmdss2  18790  frmdup1  18791  mgm2nsgrplem2  18846  mulgdirlem  19037  mulgass  19043  0nsg  19101  cycsubgcl  19138  ghmmulg  19160  conjghm  19181  qusghm  19187  gsumwrev  19298  symg2bas  19323  symgfixelsi  19365  f1otrspeq  19377  psgnunilem2  19425  psgnunilem3  19426  odf1o2  19503  lsmhash  19635  efgtf  19652  efginvrel2  19657  efgredeu  19682  efgcpbllemb  19685  frgpuplem  19702  frgpup1  19705  ghmcyg  19826  gsumval3lem1  19835  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsumzoppg  19874  gsum2d  19902  subgdmdprd  19966  pgpfac1lem3  20009  gsummgp0  20227  rnghmmul  20358  rngcinv  20546  ringcinv  20580  islmodd  20772  lmodvsmmulgdi  20803  islss3  20865  0lmhm  20947  idlmhm  20948  lmhmeql  20962  pwssplit3  20968  lidldvgen  21244  qsssubdrg  21343  cnsubrg  21344  znf1o  21461  psgnghm  21489  psgndif  21511  cssmre  21602  dsmmsubg  21652  frlmup1  21707  lindfrn  21730  f1lindf  21731  evlslem1  21989  psdmul  22053  coe1tmmul2  22162  pf1ind  22242  mamufval  22279  mamurid  22329  mvmulfval  22429  mdetralt2  22496  mndifsplit  22523  maducoeval2  22527  madugsum  22530  mat2pmatmul  22618  decpmatmul  22659  pm2mpf1lem  22681  pm2mpf1  22686  monmat2matmon  22711  chpscmat  22729  fvmptnn04if  22736  tgcl  22856  ppttop  22894  epttop  22896  clsval2  22937  opncldf1  22971  mretopd  22979  neindisj  23004  neiptopnei  23019  restcls  23068  restntr  23069  ordtbas  23079  cnpnei  23151  cncls2  23160  tgcmp  23288  cmpcld  23289  uncmp  23290  hauscmplem  23293  1stcfb  23332  2ndcctbss  23342  hauspwdom  23388  reftr  23401  comppfsc  23419  kgentopon  23425  ptpjpre1  23458  ptcnplem  23508  txcn  23513  txdis1cn  23522  txhaus  23534  xkopt  23542  imasnopn  23577  imasncld  23578  imasncls  23579  hmeoimaf1o  23657  cmphaushmeo  23687  txhmeo  23690  trfbas2  23730  fbasfip  23755  fbasrn  23771  fmss  23833  elfm2  23835  hauspwpwf1  23874  flfcnp  23891  fclscf  23912  flimfnfcls  23915  fcfval  23920  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  ptcmplem3  23941  ptcmplem4  23942  cnextfval  23949  cnextcn  23954  tmdgsum2  23983  ustex2sym  24104  neipcfilu  24183  imasdsf1olem  24261  metss2lem  24399  stdbdxmet  24403  stdbdmopn  24406  metrest  24412  metcnp  24429  restmetu  24458  tngngp  24542  icccmplem1  24711  icccvx  24848  evth  24858  lebnumlem1  24860  pi1blem  24939  isncvsngp  25049  equivcau  25200  bcthlem5  25228  cmslssbn  25272  ivthlem3  25354  ovolicc2lem3  25420  ovolicc2lem4  25421  dyaddisj  25497  dyadmbllem  25500  ismbfd  25540  itg2seq  25643  itgss  25713  limciun  25795  dvcobr  25849  dvcobrOLD  25850  dvmptfsum  25879  c1liplem1  25901  c1lip1  25902  lhop  25921  dvcvx  25925  tdeglem4  25965  plyco0  26097  elply2  26101  plypf1  26117  dgreq0  26171  elqaalem2  26228  aalioulem6  26245  aaliou  26246  aaliou2b  26249  ulmss  26306  ulmcn  26308  pserulm  26331  lgamgulmlem5  26943  basellem4  26994  fsumdvdsdiaglem  27093  mpodvdsmulf1o  27104  dvdsmulf1o  27106  chtublem  27122  fsumvma2  27125  logfaclbnd  27133  dchrelbasd  27150  lgsqrlem2  27258  gausslemma2dlem1a  27276  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  rplogsumlem2  27396  rpvmasumlem  27398  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  rpvmasum2  27423  dchrisum0lem1  27427  logsqvma  27453  selberg4  27472  pntibndlem3  27503  pntlem3  27520  ostthlem1  27538  ostthlem2  27539  sltres  27574  nogt01o  27608  oldbdayim  27800  addsproplem2  27877  negsproplem2  27935  mulsval  28012  om2noseqrdg  28198  noseqrdgfn  28200  zmulscld  28285  recut  28347  idmot  28464  brcgr  28827  brbtwn2  28832  axsegconlem8  28851  axpaschlem  28867  axeuclid  28890  axcontlem2  28892  axcontlem7  28897  eengtrkg  28913  upgrex  29019  subgrprop3  29203  subupgr  29214  nbgr0edglem  29283  nb3grprlem1  29307  cusgredg  29351  cusgrres  29376  usgredgsscusgredg  29387  finsumvtxdg2ssteplem4  29476  finsumvtxdg2sstep  29477  wlkl1loop  29566  wlkp1lem4  29604  wwlksnred  29822  wwlksnext  29823  wwlksnextwrd  29827  wpthswwlks2on  29891  clwwlknp  29966  clwwlkel  29975  wwlksext2clwwlk  29986  clwwlknonwwlknonb  30035  3wlkond  30100  1conngr  30123  eucrctshift  30172  fusgr2wsp2nb  30263  numclwwlk1lem2foa  30283  numclwwlk1lem2f1  30286  numclwlk1lem1  30298  numclwlk1lem2  30299  grpoidinvlem1  30433  grporcan  30447  ipblnfi  30784  hvmulcan2  31002  shscli  31246  spansneleq  31499  pjspansn  31506  3oalem2  31592  eigposi  31765  cnlnadjlem2  31997  stlesi  32170  mdslmd1lem1  32254  mdslmd1lem2  32255  cdj1i  32362  disjxpin  32517  nn0xmulclb  32694  xreceu  32842  txomap  33824  pstmxmet  33887  qqhghm  33978  qqhrhm  33979  measinblem  34210  cntmeas  34216  ballotlemsf1o  34505  bnj945  34763  bnj1110  34972  f1resveqaeq  35075  cvmopnlem  35265  cvmfolem  35266  cvmliftmolem2  35269  cvmlift2lem10  35299  satf00  35361  satffunlem2lem1  35391  satefvfmla0  35405  mrsubvrs  35509  wzel  35812  btwnconn1lem8  36082  btwnconn1lem9  36083  btwnconn1lem10  36084  btwnconn1lem11  36085  btwnconn1lem12  36086  finminlem  36306  nn0prpwlem  36310  fnessref  36345  refssfne  36346  fnemeet2  36355  consym1  36408  bj-finsumval0  37273  topdifinffinlem  37335  relowlssretop  37351  rdgeqoa  37358  fvineqsneu  37399  pibt2  37405  matunitlindflem1  37610  poimirlem28  37642  mblfinlem1  37651  mblfinlem3  37653  mblfinlem4  37654  ovoliunnfl  37656  mbfresfi  37660  mbfposadd  37661  itg2addnclem2  37666  itg2addnc  37668  ftc1anc  37695  frinfm  37729  fdc  37739  blssp  37750  sstotbnd  37769  isbnd2  37777  ssbnd  37782  prdstotbnd  37788  prdsbnd2  37789  ismtyres  37802  heibor1lem  37803  rrnequiv  37829  rngoisocnv  37975  crngohomfo  38000  pridlc3  38067  membpartlem19  38803  prter3  38875  ax12eq  38934  ax12el  38935  cvratlem  39415  islvol2aN  39586  4atlem4b  39594  4atlem4c  39595  4atlem4d  39596  isline2  39768  isline3  39770  pclfinclN  39944  linepsubclN  39945  pexmidlem4N  39967  diaglbN  41049  dvhvaddcl  41089  dvhvaddcomN  41090  dvhvscacl  41097  djavalN  41129  dibglbN  41160  dihatexv  41332  djhval  41392  mapdrvallem2  41639  evlselvlem  42574  evlselv  42575  mhpind  42582  prjsprellsp  42599  elrfi  42682  nacsfix  42700  eldioph2  42750  lzenom  42758  rexrabdioph  42782  irrapxlem3  42812  pellexlem5  42821  pellex  42823  pell1234qrne0  42841  pell1234qrmulcl  42843  pell14qrdich  42857  pell1qrge1  42858  pellqrex  42867  rmxypairf1o  42900  rmxycomplete  42906  monotoddzzfi  42931  congadd  42955  jm2.19lem3  42980  jm2.19lem4  42981  jm2.25  42988  jm2.26a  42989  jm2.26lem3  42990  expdiophlem1  43010  wepwsolem  43031  lmhmfgsplit  43075  aaitgo  43151  mon1psubm  43188  deg1mhm  43189  succlg  43317  ofoacom  43350  iunrelexp0  43691  isotone2  44038  mnuprdlem4  44264  relpmin  44942  disjrnmpt2  45182  mullimc  45614  mullimcf  45621  climxrre  45748  fprodcncf  45898  stoweidlem17  46015  stoweidlem27  46025  stoweidlem54  46052  fourierdlem42  46147  fourierdlem62  46166  fourierdlem73  46177  fourierdlem76  46180  fourierdlem97  46201  sge0iunmptlemfi  46411  isomenndlem  46528  imarnf1pr  47283  smonoord  47372  fvelsetpreimafv  47388  iccpartiltu  47423  sprsymrelf1lem  47492  prproropf1olem3  47506  paireqne  47512  fmtnoprmfac1  47566  prmdvdsfmtnof1lem2  47586  gricushgr  47917  grimedg  47935  cycl3grtri  47946  gpgedg2iv  48058  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  rngcinvALTV  48264  funcringcsetcALTV2lem9  48286  ringcinvALTV  48298  funcringcsetclem9ALTV  48309  lmodvsmdi  48367  lincsum  48418  lindslinindimp2lem4  48450  nn0sumshdiglemB  48609  1arymaptf1  48631  2arymaptf1  48642  dmrnxp  48825  xpco2  48845  initopropd  49232  termopropd  49233  zeroopropd  49234  oduoppcciso  49555  lanpropd  49604  ranpropd  49605