Theorem ad2antll 741

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simprr  784  simprrl  792  simprrr  793  simprr1  1238  simprr2  1239  simprr3  1240  prneimg  4823  prproe  4874  fr2nr  5639  wereu2  5659  f1oprg  6868  fvtp1g  7197  funfvima3  7235  isof1oidb  7323  isomin  7336  weniso  7353  elovmpt3rab1  7671  sorpssi  7727  resf1extb  7931  poseq  8154  suppofssd  8199  tfrlem9a  8373  oalimcl  8545  odi  8564  oeeui  8588  ralxpmap  8894  boxriin  8938  domdifsn  9048  domunsncan  9065  enfixsn  9074  disjen  9122  mapen  9129  mapxpen  9131  mapunen  9134  findcard2d  9151  unxpdomlem2  9217  unxpdomlem3  9218  isfinite2  9258  marypha1lem  9393  marypha2  9399  supmo  9412  infmo  9457  card2inf  9517  brwdom2  9535  wemapwe  9666  rankonidlem  9800  rankxplim3  9853  djulf1o  9898  djurf1o  9899  infxpenlem  9997  infxpenc2lem1  10003  infxpenc2  10006  fseqenlem1  10008  fseqenlem2  10009  infpwfien  10046  dfac12lem2  10128  infunsdom1  10195  infunsdom  10196  infmap2  10200  fin2i2  10302  fin23lem28  10324  fin23lem32  10328  fin23lem34  10330  fin23lem40  10335  isf32lem2  10338  compssiso  10358  isfin1-3  10370  fin1a2lem10  10393  fin12  10397  hsmexlem4  10413  ac6num  10463  ttukeylem7  10499  axdclem2  10504  iundom2g  10524  fpwwe2lem11  10626  pwfseqlem3  10645  winalim2  10681  winafp  10682  wunex2  10723  grur1  10805  dedekindle  11374  00id  11385  receu  11859  lt2mul2div  12093  peano5uzi  12685  uzwo  12935  qbtwnre  13225  iooshf  13453  modmul1  13960  seqcl2  14056  seqfveq2  14060  seqid2  14084  seqdistr  14089  expcl2lem  14109  mulexpz  14138  expnlbnd2  14270  hashfun  14474  hashfacen  14491  hashf1lem1  14492  elss2prb  14525  fstwrdne0  14593  swrdsb0eq  14701  swrdswrd  14742  wrd2ind  14760  swrdccatin1  14762  pfxccatin12  14770  splid  14790  repswrevw  14824  cshwidxmod  14840  cshwidx0  14843  2cshw  14850  cshweqrep  14858  cshw1  14859  wwlktovfo  14995  relexpfld  15086  relexpindlem  15100  01sqrexlem6  15298  absexpz  15356  o1rlimmul  15670  iseralt  15736  summolem2  15767  fsumf1o  15774  fsum0diag2  15834  fsummulc2  15835  cvgcmpce  15870  incexclem  15890  prodmolem2  15989  fprodcl2lem  16004  fprodmul  16014  fprodrev  16031  moddvds  16321  dvdsflip  16375  bitsf1ocnv  16502  sadcaddlem  16515  bezoutlem2  16598  bezoutlem4  16600  dfgcd2  16604  lcmgcdlem  16664  crth  16837  hashgcdlem  16847  phisum  16850  pcqcl  16916  pcid  16933  pcneg  16934  prmpwdvds  16964  pockthg  16966  4sqlem11  17015  ramub2  17074  0ram  17080  prmgaplem7  17117  prmgaplem8  17118  setscom  17240  qusval  17596  initoeu1  18068  termoeu1  18075  setcinv  18147  funcestrcsetclem9  18204  funcsetcestrclem9  18219  fullsetcestrc  18222  1stfcl  18253  2ndfcl  18254  hofpropd  18323  isacs3lem  18598  mgmhmlin  18757  mndpsuppss  18823  frmdss2  18922  frmdup1  18923  mgm2nsgrplem2  18981  mulgdirlem  19171  mulgass  19177  0nsg  19235  cycsubgcl  19277  ghmmulg  19298  conjghm  19319  qusghm  19325  gsumwrev  19436  symg2bas  19463  symgfixelsi  19505  f1otrspeq  19517  psgnunilem2  19565  psgnunilem3  19566  odf1o2  19643  lsmhash  19775  efgtf  19792  efginvrel2  19797  efgredeu  19822  efgcpbllemb  19825  frgpuplem  19842  frgpup1  19845  ghmcyg  19966  gsumval3lem1  19975  gsumzres  19979  gsumzcl2  19980  gsumzf1o  19982  gsumzaddlem  19991  gsumconst  20004  gsumzmhm  20007  gsumzoppg  20014  gsum2d  20042  subgdmdprd  20106  pgpfac1lem3  20149  gsummgp0  20399  rnghmmul  20531  rngcinv  20722  ringcinv  20756  islmodd  20965  lmodvsmmulgdi  20996  islss3  21058  0lmhm  21139  idlmhm  21140  lmhmeql  21154  pwssplit3  21160  lidldvgen  21471  qsssubdrg  21545  cnsubrg  21546  znf1o  21670  psgnghm  21699  psgndif  21721  cssmre  21812  dsmmsubg  21862  frlmup1  21917  lindfrn  21940  f1lindf  21941  evlslem1  22202  psdmul  22298  coe1tmmul2  22406  pf1ind  22484  mamufval  22518  mamurid  22568  mvmulfval  22668  mdetralt2  22735  mndifsplit  22762  maducoeval2  22766  madugsum  22769  mat2pmatmul  22857  decpmatmul  22898  pm2mpf1lem  22920  pm2mpf1  22925  monmat2matmon  22950  chpscmat  22968  fvmptnn04if  22975  tgcl  23095  ppttop  23133  epttop  23135  clsval2  23176  opncldf1  23210  mretopd  23218  neindisj  23243  neiptopnei  23258  restcls  23307  restntr  23308  ordtbas  23318  cnpnei  23390  cncls2  23399  tgcmp  23527  cmpcld  23528  uncmp  23529  hauscmplem  23532  1stcfb  23571  2ndcctbss  23581  hauspwdom  23627  reftr  23640  comppfsc  23658  kgentopon  23664  ptpjpre1  23697  ptcnplem  23747  txcn  23752  txdis1cn  23761  txhaus  23773  xkopt  23781  imasnopn  23816  imasncld  23817  imasncls  23818  hmeoimaf1o  23896  cmphaushmeo  23926  txhmeo  23929  trfbas2  23969  fbasfip  23994  fbasrn  24010  fmss  24072  elfm2  24074  hauspwpwf1  24113  flfcnp  24130  fclscf  24151  flimfnfcls  24154  fcfval  24159  alexsubALTlem2  24174  alexsubALTlem3  24175  alexsubALTlem4  24176  ptcmplem3  24180  ptcmplem4  24181  cnextfval  24188  cnextcn  24193  tmdgsum2  24222  ustex2sym  24343  neipcfilu  24421  imasdsf1olem  24499  metss2lem  24637  stdbdxmet  24641  stdbdmopn  24644  metrest  24650  metcnp  24667  restmetu  24696  tngngp  24780  icccmplem1  24949  icccvx  25078  evth  25087  lebnumlem1  25089  pi1blem  25167  isncvsngp  25277  equivcau  25428  bcthlem5  25456  cmslssbn  25500  ivthlem3  25581  ovolicc2lem3  25647  ovolicc2lem4  25648  dyaddisj  25724  dyadmbllem  25727  ismbfd  25767  itg2seq  25870  itgss  25940  limciun  26022  dvcobr  26074  dvmptfsum  26103  c1liplem1  26124  c1lip1  26125  lhop  26144  dvcvx  26148  tdeglem4  26186  plyco0  26318  elply2  26322  plypf1  26338  dgreq0  26391  elqaalem2  26450  aalioulem6  26467  aaliou  26468  aaliou2b  26471  ulmss  26526  ulmcn  26528  pserulm  26551  lgamgulmlem5  27163  basellem4  27214  fsumdvdsdiaglem  27313  mpodvdsmulf1o  27324  dvdsmulf1o  27326  chtublem  27341  fsumvma2  27344  logfaclbnd  27352  dchrelbasd  27369  lgsqrlem2  27477  gausslemma2dlem1a  27495  lgseisenlem2  27506  lgsquadlem1  27510  lgsquadlem2  27511  lgsquadlem3  27512  rplogsumlem2  27615  rpvmasumlem  27617  dchrmusum2  27624  dchrvmasumlem1  27625  dchrvmasum2lem  27626  rpvmasum2  27642  dchrisum0lem1  27646  logsqvma  27672  selberg4  27691  pntibndlem3  27722  pntlem3  27739  ostthlem1  27757  ostthlem2  27758  ltsres  27792  nogt01o  27826  oldbdayim  28048  addsproplem2  28129  negsproplem2  28188  mulsval  28268  om2noseqrdg  28463  noseqrdgfn  28465  zmulscld  28556  recut  28653  idmot  28772  brcgr  29191  brbtwn2  29196  axsegconlem8  29215  axpaschlem  29231  axeuclid  29254  axcontlem2  29256  axcontlem7  29261  eengtrkg  29277  upgrex  29383  subgrprop3  29567  subupgr  29578  nbgr0edglem  29647  nb3grprlem1  29671  cusgredg  29715  cusgrres  29739  usgredgsscusgredg  29750  finsumvtxdg2ssteplem4  29839  finsumvtxdg2sstep  29840  wlkl1loop  29928  wlkp1lem4  29965  wwlksnred  30182  wwlksnext  30183  wwlksnextwrd  30187  wpthswwlks2on  30254  clwwlknp  30329  clwwlkel  30338  wwlksext2clwwlk  30349  clwwlknonwwlknonb  30398  3wlkond  30463  1conngr  30486  eucrctshift  30535  fusgr2wsp2nb  30626  numclwwlk1lem2foa  30646  numclwwlk1lem2f1  30649  numclwlk1lem1  30661  numclwlk1lem2  30662  grpoidinvlem1  30797  grporcan  30811  ipblnfi  31148  hvmulcan2  31366  shscli  31610  spansneleq  31863  pjspansn  31870  3oalem2  31956  eigposi  32129  cnlnadjlem2  32361  stlesi  32534  mdslmd1lem1  32618  mdslmd1lem2  32619  cdj1i  32726  disjxpin  32874  nn0xmulclb  33057  xreceu  33182  txomap  34169  pstmxmet  34232  qqhghm  34323  qqhrhm  34324  measinblem  34555  cntmeas  34561  ballotlemsf1o  34849  bnj945  35107  bnj1110  35315  f1resveqaeq  35417  rankfilimbi  35438  cvmopnlem  35703  cvmfolem  35704  cvmliftmolem2  35707  cvmlift2lem10  35737  satf00  35799  satffunlem2lem1  35829  satefvfmla0  35843  mrsubvrs  35947  wzel  36247  btwnconn1lem8  36519  btwnconn1lem9  36520  btwnconn1lem10  36521  btwnconn1lem11  36522  btwnconn1lem12  36523  finminlem  36752  nn0prpwlem  36756  fnessref  36791  refssfne  36792  fnemeet2  36801  consym1  36854  bj-finsumval0  37851  topdifinffinlem  37915  relowlssretop  37931  rdgeqoa  37938  fvineqsneu  37979  pibt2  37985  matunitlindflem1  38189  poimirlem28  38221  mblfinlem1  38230  mblfinlem3  38232  mblfinlem4  38233  ovoliunnfl  38235  mbfresfi  38239  mbfposadd  38240  itg2addnclem2  38245  itg2addnc  38247  ftc1anc  38274  frinfm  38308  fdc  38318  blssp  38329  sstotbnd  38348  isbnd2  38356  ssbnd  38361  prdstotbnd  38367  prdsbnd2  38368  ismtyres  38381  heibor1lem  38382  rrnequiv  38408  rngoisocnv  38554  crngohomfo  38579  pridlc3  38646  membpartlem19  39487  prter3  39580  ax12eq  39639  ax12el  39640  cvratlem  40119  islvol2aN  40290  4atlem4b  40298  4atlem4c  40299  4atlem4d  40300  isline2  40472  isline3  40474  pclfinclN  40648  linepsubclN  40649  pexmidlem4N  40671  diaglbN  41753  dvhvaddcl  41793  dvhvaddcomN  41794  dvhvscacl  41801  djavalN  41833  dibglbN  41864  dihatexv  42036  djhval  42096  mapdrvallem2  42343  evlselvlem  43246  evlselv  43247  mhpind  43252  prjsprellsp  43269  elrfi  43351  nacsfix  43369  eldioph2  43419  lzenom  43427  rexrabdioph  43447  irrapxlem3  43477  pellexlem5  43486  pellex  43488  pell1234qrne0  43506  pell1234qrmulcl  43508  pell14qrdich  43522  pell1qrge1  43523  pellqrex  43532  rmxypairf1o  43564  rmxycomplete  43570  monotoddzzfi  43595  congadd  43619  jm2.19lem3  43644  jm2.19lem4  43645  jm2.25  43652  jm2.26a  43653  jm2.26lem3  43654  expdiophlem1  43674  wepwsolem  43695  lmhmfgsplit  43739  aaitgo  43815  mon1psubm  43852  deg1mhm  43853  succlg  43981  ofoacom  44014  iunrelexp0  44354  isotone2  44701  mnuprdlem4  44911  relpmin  45587  disjrnmpt2  45832  mullimc  46258  mullimcf  46265  climxrre  46390  fprodcncf  46540  stoweidlem17  46657  stoweidlem27  46667  stoweidlem54  46694  fourierdlem42  46789  fourierdlem62  46808  fourierdlem73  46819  fourierdlem76  46822  fourierdlem97  46843  sge0iunmptlemfi  47053  isomenndlem  47170  imarnf1pr  47942  smonoord  48037  fvelsetpreimafv  48059  iccpartiltu  48094  sprsymrelf1lem  48163  prproropf1olem3  48177  paireqne  48183  fmtnoprmfac1  48240  prmdvdsfmtnof1lem2  48260  nprmdvdsfacm1  48299  gricushgr  48605  grimedg  48623  cycl3grtri  48635  gpgedg2iv  48755  pgnbgreunbgrlem2lem1  48802  pgnbgreunbgrlem2lem2  48803  rngcinvALTV  48964  funcringcsetcALTV2lem9  48986  ringcinvALTV  48998  funcringcsetclem9ALTV  49009  lmodvsmdi  49078  lincsum  49128  lindslinindimp2lem4  49160  nn0sumshdiglemB  49319  1arymaptf1  49341  2arymaptf1  49352  dmrnxp  49534  xpco2  49554  initopropd  49940  termopropd  49941  zeroopropd  49942  oduoppcciso  50263  lanpropd  50312  ranpropd  50313