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  4830  prproe  4881  fr2nr  5631  wereu2  5651  f1oprg  6863  fvtp1g  7190  funfvima3  7228  isof1oidb  7317  isomin  7330  weniso  7347  elovmpt3rab1  7667  sorpssi  7723  resf1extb  7930  poseq  8157  suppofssd  8202  tfrlem9a  8400  oalimcl  8572  odi  8591  oeeui  8614  ralxpmap  8910  boxriin  8954  domdifsn  9068  domunsncan  9086  enfixsn  9095  disjen  9148  mapen  9155  mapxpen  9157  mapunen  9160  findcard2d  9180  unxpdomlem2  9259  unxpdomlem3  9260  findcard3OLD  9291  isfinite2  9306  marypha1lem  9445  marypha2  9451  supmo  9464  infmo  9509  card2inf  9569  brwdom2  9587  wemapwe  9711  rankonidlem  9842  rankxplim3  9895  djulf1o  9926  djurf1o  9927  infxpenlem  10027  infxpenc2lem1  10033  infxpenc2  10036  fseqenlem1  10038  fseqenlem2  10039  infpwfien  10076  dfac12lem2  10159  infunsdom1  10226  infunsdom  10227  infmap2  10231  fin2i2  10332  fin23lem28  10354  fin23lem32  10358  fin23lem34  10360  fin23lem40  10365  isf32lem2  10368  compssiso  10388  isfin1-3  10400  fin1a2lem10  10423  fin12  10427  hsmexlem4  10443  ac6num  10493  ttukeylem7  10529  axdclem2  10534  iundom2g  10554  fpwwe2lem11  10655  pwfseqlem3  10674  winalim2  10710  winafp  10711  wunex2  10752  grur1  10834  dedekindle  11399  00id  11410  receu  11882  lt2mul2div  12120  peano5uzi  12682  uzwo  12927  qbtwnre  13215  iooshf  13443  modmul1  13942  seqcl2  14038  seqfveq2  14042  seqid2  14066  seqdistr  14071  expcl2lem  14091  mulexpz  14120  expnlbnd2  14252  hashfun  14455  hashfacen  14472  hashf1lem1  14473  elss2prb  14506  fstwrdne0  14574  swrdsb0eq  14681  swrdswrd  14723  wrd2ind  14741  swrdccatin1  14743  pfxccatin12  14751  splid  14771  repswrevw  14805  cshwidxmod  14821  cshwidx0  14824  2cshw  14831  cshweqrep  14839  cshw1  14840  wwlktovfo  14977  relexpfld  15068  relexpindlem  15082  01sqrexlem6  15266  absexpz  15324  o1rlimmul  15635  iseralt  15701  summolem2  15732  fsumf1o  15739  fsum0diag2  15799  fsummulc2  15800  cvgcmpce  15834  incexclem  15852  prodmolem2  15951  fprodcl2lem  15966  fprodmul  15976  fprodrev  15993  moddvds  16283  dvdsflip  16336  bitsf1ocnv  16463  sadcaddlem  16476  bezoutlem2  16559  bezoutlem4  16561  dfgcd2  16565  lcmgcdlem  16625  crth  16797  hashgcdlem  16807  phisum  16810  pcqcl  16876  pcid  16893  pcneg  16894  prmpwdvds  16924  pockthg  16926  4sqlem11  16975  ramub2  17034  0ram  17040  prmgaplem7  17077  prmgaplem8  17078  setscom  17199  qusval  17556  initoeu1  18024  termoeu1  18031  setcinv  18103  funcestrcsetclem9  18160  funcsetcestrclem9  18175  fullsetcestrc  18178  1stfcl  18209  2ndfcl  18210  hofpropd  18279  isacs3lem  18552  mgmhmlin  18677  mndpsuppss  18743  frmdss2  18841  frmdup1  18842  mgm2nsgrplem2  18897  mulgdirlem  19088  mulgass  19094  0nsg  19152  cycsubgcl  19189  ghmmulg  19211  conjghm  19232  qusghm  19238  gsumwrev  19349  symg2bas  19374  symgfixelsi  19416  f1otrspeq  19428  psgnunilem2  19476  psgnunilem3  19477  odf1o2  19554  lsmhash  19686  efgtf  19703  efginvrel2  19708  efgredeu  19733  efgcpbllemb  19736  frgpuplem  19753  frgpup1  19756  ghmcyg  19877  gsumval3lem1  19886  gsumzres  19890  gsumzcl2  19891  gsumzf1o  19893  gsumzaddlem  19902  gsumconst  19915  gsumzmhm  19918  gsumzoppg  19925  gsum2d  19953  subgdmdprd  20017  pgpfac1lem3  20060  gsummgp0  20278  rnghmmul  20409  rngcinv  20597  ringcinv  20631  islmodd  20823  lmodvsmmulgdi  20854  islss3  20916  0lmhm  20998  idlmhm  20999  lmhmeql  21013  pwssplit3  21019  lidldvgen  21295  qsssubdrg  21394  cnsubrg  21395  znf1o  21512  psgnghm  21540  psgndif  21562  cssmre  21653  dsmmsubg  21703  frlmup1  21758  lindfrn  21781  f1lindf  21782  evlslem1  22040  psdmul  22104  coe1tmmul2  22213  pf1ind  22293  mamufval  22330  mamurid  22380  mvmulfval  22480  mdetralt2  22547  mndifsplit  22574  maducoeval2  22578  madugsum  22581  mat2pmatmul  22669  decpmatmul  22710  pm2mpf1lem  22732  pm2mpf1  22737  monmat2matmon  22762  chpscmat  22780  fvmptnn04if  22787  tgcl  22907  ppttop  22945  epttop  22947  clsval2  22988  opncldf1  23022  mretopd  23030  neindisj  23055  neiptopnei  23070  restcls  23119  restntr  23120  ordtbas  23130  cnpnei  23202  cncls2  23211  tgcmp  23339  cmpcld  23340  uncmp  23341  hauscmplem  23344  1stcfb  23383  2ndcctbss  23393  hauspwdom  23439  reftr  23452  comppfsc  23470  kgentopon  23476  ptpjpre1  23509  ptcnplem  23559  txcn  23564  txdis1cn  23573  txhaus  23585  xkopt  23593  imasnopn  23628  imasncld  23629  imasncls  23630  hmeoimaf1o  23708  cmphaushmeo  23738  txhmeo  23741  trfbas2  23781  fbasfip  23806  fbasrn  23822  fmss  23884  elfm2  23886  hauspwpwf1  23925  flfcnp  23942  fclscf  23963  flimfnfcls  23966  fcfval  23971  alexsubALTlem2  23986  alexsubALTlem3  23987  alexsubALTlem4  23988  ptcmplem3  23992  ptcmplem4  23993  cnextfval  24000  cnextcn  24005  tmdgsum2  24034  ustex2sym  24155  neipcfilu  24234  imasdsf1olem  24312  metss2lem  24450  stdbdxmet  24454  stdbdmopn  24457  metrest  24463  metcnp  24480  restmetu  24509  tngngp  24593  icccmplem1  24762  icccvx  24899  evth  24909  lebnumlem1  24911  pi1blem  24990  isncvsngp  25101  equivcau  25252  bcthlem5  25280  cmslssbn  25324  ivthlem3  25406  ovolicc2lem3  25472  ovolicc2lem4  25473  dyaddisj  25549  dyadmbllem  25552  ismbfd  25592  itg2seq  25695  itgss  25765  limciun  25847  dvcobr  25901  dvcobrOLD  25902  dvmptfsum  25931  c1liplem1  25953  c1lip1  25954  lhop  25973  dvcvx  25977  tdeglem4  26017  plyco0  26149  elply2  26153  plypf1  26169  dgreq0  26223  elqaalem2  26280  aalioulem6  26297  aaliou  26298  aaliou2b  26301  ulmss  26358  ulmcn  26360  pserulm  26383  lgamgulmlem5  26995  basellem4  27046  fsumdvdsdiaglem  27145  mpodvdsmulf1o  27156  dvdsmulf1o  27158  chtublem  27174  fsumvma2  27177  logfaclbnd  27185  dchrelbasd  27202  lgsqrlem2  27310  gausslemma2dlem1a  27328  lgseisenlem2  27339  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  rplogsumlem2  27448  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  rpvmasum2  27475  dchrisum0lem1  27479  logsqvma  27505  selberg4  27524  pntibndlem3  27555  pntlem3  27572  ostthlem1  27590  ostthlem2  27591  sltres  27626  nogt01o  27660  oldbdayim  27852  addsproplem2  27929  negsproplem2  27987  mulsval  28064  om2noseqrdg  28250  noseqrdgfn  28252  zmulscld  28337  recut  28399  idmot  28516  brcgr  28879  brbtwn2  28884  axsegconlem8  28903  axpaschlem  28919  axeuclid  28942  axcontlem2  28944  axcontlem7  28949  eengtrkg  28965  upgrex  29071  subgrprop3  29255  subupgr  29266  nbgr0edglem  29335  nb3grprlem1  29359  cusgredg  29403  cusgrres  29428  usgredgsscusgredg  29439  finsumvtxdg2ssteplem4  29528  finsumvtxdg2sstep  29529  wlkl1loop  29618  wlkp1lem4  29656  wwlksnred  29874  wwlksnext  29875  wwlksnextwrd  29879  wpthswwlks2on  29943  clwwlknp  30018  clwwlkel  30027  wwlksext2clwwlk  30038  clwwlknonwwlknonb  30087  3wlkond  30152  1conngr  30175  eucrctshift  30224  fusgr2wsp2nb  30315  numclwwlk1lem2foa  30335  numclwwlk1lem2f1  30338  numclwlk1lem1  30350  numclwlk1lem2  30351  grpoidinvlem1  30485  grporcan  30499  ipblnfi  30836  hvmulcan2  31054  shscli  31298  spansneleq  31551  pjspansn  31558  3oalem2  31644  eigposi  31817  cnlnadjlem2  32049  stlesi  32222  mdslmd1lem1  32306  mdslmd1lem2  32307  cdj1i  32414  disjxpin  32569  nn0xmulclb  32748  xreceu  32896  txomap  33865  pstmxmet  33928  qqhghm  34019  qqhrhm  34020  measinblem  34251  cntmeas  34257  ballotlemsf1o  34546  bnj945  34804  bnj1110  35013  f1resveqaeq  35116  cvmopnlem  35300  cvmfolem  35301  cvmliftmolem2  35304  cvmlift2lem10  35334  satf00  35396  satffunlem2lem1  35426  satefvfmla0  35440  mrsubvrs  35544  wzel  35842  btwnconn1lem8  36112  btwnconn1lem9  36113  btwnconn1lem10  36114  btwnconn1lem11  36115  btwnconn1lem12  36116  finminlem  36336  nn0prpwlem  36340  fnessref  36375  refssfne  36376  fnemeet2  36385  consym1  36438  bj-finsumval0  37303  topdifinffinlem  37365  relowlssretop  37381  rdgeqoa  37388  fvineqsneu  37429  pibt2  37435  matunitlindflem1  37640  poimirlem28  37672  mblfinlem1  37681  mblfinlem3  37683  mblfinlem4  37684  ovoliunnfl  37686  mbfresfi  37690  mbfposadd  37691  itg2addnclem2  37696  itg2addnc  37698  ftc1anc  37725  frinfm  37759  fdc  37769  blssp  37780  sstotbnd  37799  isbnd2  37807  ssbnd  37812  prdstotbnd  37818  prdsbnd2  37819  ismtyres  37832  heibor1lem  37833  rrnequiv  37859  rngoisocnv  38005  crngohomfo  38030  pridlc3  38097  membpartlem19  38829  prter3  38900  ax12eq  38959  ax12el  38960  cvratlem  39440  islvol2aN  39611  4atlem4b  39619  4atlem4c  39620  4atlem4d  39621  isline2  39793  isline3  39795  pclfinclN  39969  linepsubclN  39970  pexmidlem4N  39992  diaglbN  41074  dvhvaddcl  41114  dvhvaddcomN  41115  dvhvscacl  41122  djavalN  41154  dibglbN  41185  dihatexv  41357  djhval  41417  mapdrvallem2  41664  metakunt15  42232  evlselvlem  42609  evlselv  42610  mhpind  42617  prjsprellsp  42634  elrfi  42717  nacsfix  42735  eldioph2  42785  lzenom  42793  rexrabdioph  42817  irrapxlem3  42847  pellexlem5  42856  pellex  42858  pell1234qrne0  42876  pell1234qrmulcl  42878  pell14qrdich  42892  pell1qrge1  42893  pellqrex  42902  rmxypairf1o  42935  rmxycomplete  42941  monotoddzzfi  42966  congadd  42990  jm2.19lem3  43015  jm2.19lem4  43016  jm2.25  43023  jm2.26a  43024  jm2.26lem3  43025  expdiophlem1  43045  wepwsolem  43066  lmhmfgsplit  43110  aaitgo  43186  mon1psubm  43223  deg1mhm  43224  succlg  43352  ofoacom  43385  iunrelexp0  43726  isotone2  44073  mnuprdlem4  44299  relpmin  44977  disjrnmpt2  45212  mullimc  45645  mullimcf  45652  climxrre  45779  fprodcncf  45929  stoweidlem17  46046  stoweidlem27  46056  stoweidlem54  46083  fourierdlem42  46178  fourierdlem62  46197  fourierdlem73  46208  fourierdlem76  46211  fourierdlem97  46232  sge0iunmptlemfi  46442  isomenndlem  46559  imarnf1pr  47311  smonoord  47385  fvelsetpreimafv  47401  iccpartiltu  47436  sprsymrelf1lem  47505  prproropf1olem3  47519  paireqne  47525  fmtnoprmfac1  47579  prmdvdsfmtnof1lem2  47599  gricushgr  47930  grimedg  47948  cycl3grtri  47959  rngcinvALTV  48251  funcringcsetcALTV2lem9  48273  ringcinvALTV  48285  funcringcsetclem9ALTV  48296  lmodvsmdi  48354  lincsum  48405  lindslinindimp2lem4  48437  nn0sumshdiglemB  48600  1arymaptf1  48622  2arymaptf1  48633  dmrnxp  48815  initopropd  49160  termopropd  49161  zeroopropd  49162  oduoppcciso  49443