Theorem ad2antll 742

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simprr  785  simprrl  793  simprrr  794  simprr1  1240  simprr2  1241  simprr3  1242  prneimg  4814  prproe  4865  fr2nr  5628  wereu2  5648  f1oprg  6871  fvtp1g  7203  funfvima3  7242  f1resveqaeq  7277  isof1oidb  7332  isomin  7345  weniso  7364  elovmpt3rab1  7681  sorpssi  7745  resf1extb  7946  poseq  8175  suppofssd  8220  tfrlem9a  8394  oalimcl  8568  odi  8587  oeeui  8611  ralxpmap  8924  boxriin  8968  domdifsn  9079  domunsncan  9096  enfixsn  9105  disjen  9153  mapen  9160  mapxpen  9162  mapunen  9165  findcard2d  9182  unxpdomlem2  9248  unxpdomlem3  9249  isfinite2  9290  marypha1lem  9425  marypha2  9431  supmo  9444  infmo  9489  card2inf  9549  brwdom2  9567  wemapwe  9698  rankonidlem  9838  rankxplim3  9898  rankfilimbi  9902  djulf1o  9993  djurf1o  9994  infxpenlem  10092  infxpenc2lem1  10098  infxpenc2  10101  fseqenlem1  10103  fseqenlem2  10104  infpwfien  10141  dfac12lem2  10223  infunsdom1  10290  infunsdom  10291  infmap2  10295  fin2i2  10396  fin23lem28  10418  fin23lem32  10422  fin23lem34  10424  fin23lem40  10429  isf32lem2  10432  compssiso  10452  isfin1-3  10464  fin1a2lem10  10487  fin12  10491  hsmexlem4  10507  ac6num  10557  ttukeylem7  10593  axdclem2  10598  iundom2g  10624  fpwwe2lem11  10726  pwfseqlem3  10745  winalim2  10781  winafp  10782  wunex2  10823  grur1  10905  dedekindle  11474  00id  11485  receu  11961  lt2mul2div  12195  peano5uzi  12788  uzwo  13038  qbtwnre  13329  iooshf  13557  modmul1  14067  seqcl2  14163  seqfveq2  14167  seqid2  14191  seqdistr  14196  expcl2lem  14216  mulexpz  14245  expnlbnd2  14378  hashfun  14582  hashfacen  14599  hashf1lem1  14600  elss2prb  14633  fstwrdne0  14701  swrdsb0eq  14813  swrdswrd  14854  wrd2ind  14872  swrdccatin1  14874  pfxccatin12  14882  splid  14902  repswrevw  14938  cshwidxmod  14954  cshwidx0  14957  2cshw  14964  cshweqrep  14972  cshw1  14973  wwlktovfo  15111  relexpfld  15202  relexpindlem  15216  01sqrexlem6  15414  absexpz  15472  o1rlimmul  15786  iseralt  15852  summolem2  15882  fsumf1o  15889  fsum0diag2  15949  fsummulc2  15950  cvgcmpce  15985  incexclem  16005  prodmolem2  16102  fprodcl2lem  16117  fprodmul  16127  fprodrev  16144  moddvds  16433  dvdsflip  16487  bitsf1ocnv  16614  sadcaddlem  16627  bezoutlem2  16713  bezoutlem4  16715  dfgcd2  16719  lcmgcdlem  16781  crth  16955  hashgcdlem  16965  phisum  16968  pcqcl  17034  pcid  17051  pcneg  17052  prmpwdvds  17082  pockthg  17084  4sqlem11  17133  ramub2  17192  0ram  17198  prmgaplem7  17235  prmgaplem8  17236  setscom  17358  qusval  17714  initoeu1  18186  termoeu1  18193  setcinv  18265  funcestrcsetclem9  18322  funcsetcestrclem9  18337  fullsetcestrc  18340  1stfcl  18371  2ndfcl  18372  hofpropd  18441  isacs3lem  18716  mgmhmlin  18888  mndpsuppss  18959  frmdss2  19059  frmdup1  19060  mgm2nsgrplem2  19118  mulgdirlem  19315  mulgass  19321  0nsg  19379  cycsubgcl  19421  ghmmulg  19442  conjghm  19463  qusghm  19469  gsumwrev  19580  symg2bas  19607  symgfixelsi  19649  f1otrspeq  19661  psgnunilem2  19709  psgnunilem3  19710  odf1o2  19787  lsmhash  19919  efgtf  19936  efginvrel2  19941  efgredeu  19966  efgcpbllemb  19969  frgpuplem  19986  frgpup1  19989  ghmcyg  20110  gsumval3lem1  20119  gsumzres  20123  gsumzcl2  20124  gsumzf1o  20126  gsumzaddlem  20135  gsumconst  20148  gsumzmhm  20151  gsumzoppg  20158  gsum2d  20186  subgdmdprd  20250  pgpfac1lem3  20293  gsummgp0  20547  rnghmmul  20679  rngcinv  20889  ringcinv  20923  islmodd  21141  lmodvsmmulgdi  21172  islss3  21234  0lmhm  21315  idlmhm  21316  lmhmeql  21330  pwssplit3  21336  cmprmidlmcl  21631  lidldvgen  21658  qsssubdrg  21732  cnsubrg  21733  znf1o  21857  psgnghm  21886  psgndif  21908  cssmre  21999  dsmmsubg  22049  frlmup1  22104  lindfrn  22127  f1lindf  22128  evlslem1  22391  psdmul  22487  coe1tmmul2  22595  pf1ind  22673  mamufval  22707  mamurid  22757  mvmulfval  22857  mdetralt2  22924  mndifsplit  22951  maducoeval2  22955  madugsum  22958  matunitlindflem1  22994  mat2pmatmul  23049  decpmatmul  23090  pm2mpf1lem  23112  pm2mpf1  23117  monmat2matmon  23142  chpscmat  23160  fvmptnn04if  23167  tgcl  23287  ppttop  23325  epttop  23327  clsval2  23368  opncldf1  23402  mretopd  23410  neindisj  23435  neiptopnei  23450  restcls  23499  restntr  23500  ordtbas  23510  cnpnei  23582  cncls2  23591  tgcmp  23719  cmpcld  23720  uncmp  23721  hauscmplem  23724  1stcfb  23763  2ndcctbss  23774  hauspwdom  23820  reftr  23833  comppfsc  23851  kgentopon  23857  ptpjpre1  23890  ptcnplem  23940  txcn  23945  txdis1cn  23954  txhaus  23966  xkopt  23974  imasnopn  24009  imasncld  24010  imasncls  24011  hmeoimaf1o  24089  cmphaushmeo  24119  txhmeo  24122  trfbas2  24162  fbasfip  24187  fbasrn  24203  fmss  24265  elfm2  24267  hauspwpwf1  24306  flfcnp  24323  fclscf  24344  flimfnfcls  24347  fcfval  24352  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  ptcmplem3  24373  ptcmplem4  24374  cnextfval  24381  cnextcn  24386  tmdgsum2  24415  ustex2sym  24536  neipcfilu  24614  imasdsf1olem  24692  metss2lem  24830  stdbdxmet  24834  stdbdmopn  24837  metrest  24843  metcnp  24860  restmetu  24889  tngngp  24973  icccmplem1  25142  icccvx  25271  evth  25280  lebnumlem1  25282  pi1blem  25360  isncvsngp  25470  equivcau  25621  bcthlem5  25649  cmslssbn  25693  ivthlem3  25774  ovolicc2lem3  25840  ovolicc2lem4  25841  dyaddisj  25917  dyadmbllem  25920  ismbfd  25960  itg2seq  26063  itgss  26132  limciun  26214  dvcobr  26266  dvmptfsum  26295  c1liplem1  26316  c1lip1  26317  lhop  26336  dvcvx  26340  tdeglem4  26378  plyco0  26510  elply2  26514  plypf1  26531  dgreq0  26584  elqaalem2  26643  aalioulem6  26664  aaliou  26665  aaliou2b  26668  ulmss  26724  ulmcn  26726  pserulm  26749  lgamgulmlem5  27360  basellem4  27411  fsumdvdsdiaglem  27510  mpodvdsmulf1o  27521  dvdsmulf1o  27523  chtublem  27538  fsumvma2  27541  logfaclbnd  27549  dchrelbasd  27566  lgsqrlem2  27674  gausslemma2dlem1a  27692  lgseisenlem2  27703  lgsquadlem1  27707  lgsquadlem2  27708  lgsquadlem3  27709  rplogsumlem2  27812  rpvmasumlem  27814  dchrmusum2  27821  dchrvmasumlem1  27822  dchrvmasum2lem  27823  rpvmasum2  27839  dchrisum0lem1  27843  logsqvma  27869  selberg4  27888  pntibndlem3  27919  pntlem3  27936  ostthlem1  27954  ostthlem2  27955  ltsres  28019  nogt01o  28053  oldbdayim  28275  addsproplem2  28356  negsproplem2  28415  mulsval  28495  om2noseqrdg  28690  noseqrdgfn  28692  zmulscld  28783  recut  28880  idmot  29000  brcgr  29478  brbtwn2  29483  axsegconlem8  29502  axpaschlem  29518  axeuclid  29541  axcontlem2  29543  axcontlem7  29548  eengtrkg  29564  upgrex  29670  subgrprop3  29857  subupgr  29868  nbgr0edglem  29937  nb3grprlem1  29961  cusgredg  30005  cusgrres  30029  usgredgsscusgredg  30040  finsumvtxdg2ssteplem4  30129  finsumvtxdg2sstep  30130  wlkl1loop  30218  wlkp1lem4  30255  wwlksnred  30481  wwlksnext  30482  wwlksnextwrd  30486  wpthswwlks2on  30553  clwwlknp  30628  clwwlkel  30637  wwlksext2clwwlk  30648  clwwlknonwwlknonb  30697  3wlkond  30772  1conngr  30795  eucrctshift  30844  fusgr2wsp2nb  30935  numclwwlk1lem2foa  30955  numclwwlk1lem2f1  30958  numclwlk1lem1  30970  numclwlk1lem2  30971  grpoidinvlem1  31106  grporcan  31120  ipblnfi  31457  hvmulcan2  31675  shscli  31919  spansneleq  32172  pjspansn  32179  3oalem2  32265  eigposi  32438  cnlnadjlem2  32670  stlesi  32843  mdslmd1lem1  32927  mdslmd1lem2  32928  cdj1i  33035  disjxpin  33182  nn0xmulclb  33363  xreceu  33488  txomap  34466  pstmxmet  34529  qqhghm  34620  qqhrhm  34621  measinblem  34853  cntmeas  34859  ballotlemsf1o  35146  bnj945  35404  bnj1110  35612  cvmopnlem  36043  cvmfolem  36044  cvmliftmolem2  36047  cvmlift2lem10  36077  satf00  36139  satffunlem2lem1  36169  satefvfmla0  36183  mrsubvrs  36287  wzel  36586  btwnconn1lem8  36859  btwnconn1lem9  36860  btwnconn1lem10  36861  btwnconn1lem11  36862  btwnconn1lem12  36863  finminlem  37106  nn0prpwlem  37110  fnessref  37145  refssfne  37146  fnemeet2  37155  consym1  37208  bj-finsumval0  38206  topdifinffinlem  38270  relowlssretop  38286  rdgeqoa  38293  fvineqsneu  38334  pibt2  38340  poimirlem28  38566  mblfinlem1  38575  mblfinlem3  38577  mblfinlem4  38578  ovoliunnfl  38580  mbfresfi  38584  mbfposadd  38585  itg2addnclem2  38590  itg2addnc  38592  ftc1anc  38619  frinfm  38669  fdc  38679  blssp  38690  sstotbnd  38709  isbnd2  38717  ssbnd  38722  prdstotbnd  38728  prdsbnd2  38729  ismtyres  38742  heibor1lem  38743  rrnequiv  38769  rngoisocnv  38915  crngohomfo  38940  pridlc3  39007  membpartlem19  39846  prter3  39939  ax12eq  39998  ax12el  39999  cvratlem  40478  islvol2aN  40649  4atlem4b  40657  4atlem4c  40658  4atlem4d  40659  isline2  40831  isline3  40833  pclfinclN  41007  linepsubclN  41008  pexmidlem4N  41030  diaglbN  42112  dvhvaddcl  42152  dvhvaddcomN  42153  dvhvscacl  42160  djavalN  42192  dibglbN  42223  dihatexv  42395  djhval  42455  mapdrvallem2  42702  evlselvlem  43616  evlselv  43617  mhpind  43622  prjsprellsp  43639  elrfi  43704  nacsfix  43722  eldioph2  43772  lzenom  43780  rexrabdioph  43800  irrapxlem3  43830  pellexlem5  43839  pellex  43841  pell1234qrne0  43859  pell1234qrmulcl  43861  pell14qrdich  43875  pell1qrge1  43876  pellqrex  43885  rmxypairf1o  43917  rmxycomplete  43923  monotoddzzfi  43948  congadd  43972  jm2.19lem3  43997  jm2.19lem4  43998  jm2.25  44005  jm2.26a  44006  jm2.26lem3  44007  expdiophlem1  44027  wepwsolem  44048  lmhmfgsplit  44087  aaitgo  44163  mon1psubm  44200  deg1mhm  44201  succlg  44329  ofoacom  44362  iunrelexp0  44701  isotone2  45048  mnuprdlem4  45258  relpmin  45941  disjrnmpt2  46202  mullimc  46627  mullimcf  46634  climxrre  46759  fprodcncf  46909  stoweidlem17  47026  stoweidlem27  47036  stoweidlem54  47063  fourierdlem42  47158  fourierdlem62  47177  fourierdlem73  47188  fourierdlem76  47191  fourierdlem97  47212  sge0iunmptlemfi  47422  isomenndlem  47539  imarnf1pr  48351  smonoord  48446  fvelsetpreimafv  48468  iccpartiltu  48503  sprsymrelf1lem  48572  prproropf1olem3  48586  paireqne  48592  fmtnoprmfac1  48649  prmdvdsfmtnof1lem2  48669  nprmdvdsfacm1  48708  gricushgr  49014  grimedg  49032  cycl3grtri  49044  gpgedg2iv  49164  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  rngcinvALTV  49372  funcringcsetcALTV2lem9  49394  ringcinvALTV  49406  funcringcsetclem9ALTV  49417  lmodvsmdi  49490  lincsum  49540  lindslinindimp2lem4  49572  nn0sumshdiglemB  49731  1arymaptf1  49753  2arymaptf1  49764  dmrnxp  49946  xpco2  49966  initopropd  50350  termopropd  50351  zeroopropd  50352  oduoppcciso  50673  lanpropd  50722  ranpropd  50723