Theorem ad2antll 728

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  simprr  772  simprrl  780  simprrr  781  simprr1  1222  simprr2  1223  simprr3  1224  prneimg  4856  fr2nr  5655  wereu2  5674  f1oprg  6879  fvtp1g  7199  funfvima3  7238  isof1oidb  7321  isomin  7334  weniso  7351  elovmpt3rab1  7666  sorpssi  7719  poseq  8144  suppofssd  8188  tfrlem9a  8386  oalimcl  8560  odi  8579  oeeui  8602  ralxpmap  8890  boxriin  8934  domdifsn  9054  domunsncan  9072  enfixsn  9081  disjen  9134  mapen  9141  mapxpen  9143  mapunen  9146  findcard2d  9166  unxpdomlem2  9251  unxpdomlem3  9252  findcard3OLD  9286  isfinite2  9301  marypha1lem  9428  marypha2  9434  supmo  9447  infmo  9490  card2inf  9550  brwdom2  9568  wemapwe  9692  rankonidlem  9823  rankxplim3  9876  djulf1o  9907  djurf1o  9908  infxpenlem  10008  infxpenc2lem1  10014  infxpenc2  10017  fseqenlem1  10019  fseqenlem2  10020  infpwfien  10057  dfac12lem2  10139  infunsdom1  10208  infunsdom  10209  infmap2  10213  fin2i2  10313  fin23lem28  10335  fin23lem32  10339  fin23lem34  10341  fin23lem40  10346  isf32lem2  10349  compssiso  10369  isfin1-3  10381  fin1a2lem10  10404  fin12  10408  hsmexlem4  10424  ac6num  10474  ttukeylem7  10510  axdclem2  10515  iundom2g  10535  fpwwe2lem11  10636  pwfseqlem3  10655  winalim2  10691  winafp  10692  wunex2  10733  grur1  10815  dedekindle  11378  00id  11389  receu  11859  lt2mul2div  12092  peano5uzi  12651  uzwo  12895  qbtwnre  13178  iooshf  13403  modmul1  13889  seqcl2  13986  seqfveq2  13990  seqid2  14014  seqdistr  14019  expcl2lem  14039  mulexpz  14068  expnlbnd2  14197  hashfun  14397  hashfacen  14413  hashfacenOLD  14414  hashf1lem1  14415  hashf1lem1OLD  14416  elss2prb  14448  fstwrdne0  14506  swrdsb0eq  14613  swrdswrd  14655  wrd2ind  14673  swrdccatin1  14675  pfxccatin12  14683  splid  14703  repswrevw  14737  cshwidxmod  14753  cshwidx0  14756  2cshw  14763  cshweqrep  14771  cshw1  14772  wwlktovfo  14909  relexpfld  14996  relexpindlem  15010  01sqrexlem6  15194  absexpz  15252  o1rlimmul  15563  iseralt  15631  summolem2  15662  fsumf1o  15669  fsum0diag2  15729  fsummulc2  15730  cvgcmpce  15764  incexclem  15782  prodmolem2  15879  fprodcl2lem  15894  fprodmul  15904  fprodrev  15921  moddvds  16208  dvdsflip  16260  bitsf1ocnv  16385  sadcaddlem  16398  bezoutlem2  16482  bezoutlem4  16484  dfgcd2  16488  lcmgcdlem  16543  crth  16711  hashgcdlem  16721  phisum  16723  pcqcl  16789  pcid  16806  pcneg  16807  prmpwdvds  16837  pockthg  16839  4sqlem11  16888  ramub2  16947  0ram  16953  prmgaplem7  16990  prmgaplem8  16991  setscom  17113  qusval  17488  initoeu1  17961  termoeu1  17968  setcinv  18040  funcestrcsetclem9  18100  funcsetcestrclem9  18115  fullsetcestrc  18118  1stfcl  18149  2ndfcl  18150  hofpropd  18220  isacs3lem  18495  frmdss2  18744  frmdup1  18745  mgm2nsgrplem2  18800  mulgdirlem  18985  mulgass  18991  0nsg  19049  cycsubgcl  19083  ghmmulg  19104  conjghm  19123  qusghm  19129  gsumwrev  19233  symg2bas  19260  symgfixelsi  19303  f1otrspeq  19315  psgnunilem2  19363  psgnunilem3  19364  odf1o2  19441  lsmhash  19573  efgtf  19590  efginvrel2  19595  efgredeu  19620  efgcpbllemb  19623  frgpuplem  19640  frgpup1  19643  ghmcyg  19764  gsumval3lem1  19773  gsumzres  19777  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumconst  19802  gsumzmhm  19805  gsumzoppg  19812  gsum2d  19840  subgdmdprd  19904  pgpfac1lem3  19947  gsummgp0  20130  islmodd  20477  lmodvsmmulgdi  20507  islss3  20570  0lmhm  20651  idlmhm  20652  lmhmeql  20666  pwssplit3  20672  lidldvgen  20893  qsssubdrg  21004  cnsubrg  21005  znf1o  21107  psgnghm  21133  psgndif  21155  cssmre  21246  dsmmsubg  21298  frlmup1  21353  lindfrn  21376  f1lindf  21377  evlslem1  21645  coe1tmmul2  21798  pf1ind  21874  mamufval  21887  mamurid  21944  mvmulfval  22044  mdetralt2  22111  mndifsplit  22138  maducoeval2  22142  madugsum  22145  mat2pmatmul  22233  decpmatmul  22274  pm2mpf1lem  22296  pm2mpf1  22301  monmat2matmon  22326  chpscmat  22344  fvmptnn04if  22351  tgcl  22472  ppttop  22510  epttop  22512  clsval2  22554  opncldf1  22588  mretopd  22596  neindisj  22621  neiptopnei  22636  restcls  22685  restntr  22686  ordtbas  22696  cnpnei  22768  cncls2  22777  tgcmp  22905  cmpcld  22906  uncmp  22907  hauscmplem  22910  1stcfb  22949  2ndcctbss  22959  hauspwdom  23005  reftr  23018  comppfsc  23036  kgentopon  23042  ptpjpre1  23075  ptcnplem  23125  txcn  23130  txdis1cn  23139  txhaus  23151  xkopt  23159  imasnopn  23194  imasncld  23195  imasncls  23196  hmeoimaf1o  23274  cmphaushmeo  23304  txhmeo  23307  trfbas2  23347  fbasfip  23372  fbasrn  23388  fmss  23450  elfm2  23452  hauspwpwf1  23491  flfcnp  23508  fclscf  23529  flimfnfcls  23532  fcfval  23537  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  ptcmplem3  23558  ptcmplem4  23559  cnextfval  23566  cnextcn  23571  tmdgsum2  23600  ustex2sym  23721  neipcfilu  23801  imasdsf1olem  23879  metss2lem  24020  stdbdxmet  24024  stdbdmopn  24027  metrest  24033  metcnp  24050  restmetu  24079  tngngp  24171  icccmplem1  24338  icccvx  24466  evth  24475  lebnumlem1  24477  pi1blem  24555  isncvsngp  24666  equivcau  24817  bcthlem5  24845  cmslssbn  24889  ivthlem3  24970  ovolicc2lem3  25036  ovolicc2lem4  25037  dyaddisj  25113  dyadmbllem  25116  ismbfd  25156  itg2seq  25260  itgss  25329  limciun  25411  dvcobr  25463  dvmptfsum  25492  c1liplem1  25513  c1lip1  25514  lhop  25533  dvcvx  25537  tdeglem4  25577  plyco0  25706  elply2  25710  plypf1  25726  dgreq0  25779  elqaalem2  25833  aalioulem6  25850  aaliou  25851  aaliou2b  25854  ulmss  25909  ulmcn  25911  pserulm  25934  lgamgulmlem5  26537  basellem4  26588  fsumdvdsdiaglem  26687  dvdsmulf1o  26698  chtublem  26714  fsumvma2  26717  logfaclbnd  26725  dchrelbasd  26742  lgsqrlem2  26850  gausslemma2dlem1a  26868  lgseisenlem2  26879  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  rplogsumlem2  26988  rpvmasumlem  26990  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasum2lem  26999  rpvmasum2  27015  dchrisum0lem1  27019  logsqvma  27045  selberg4  27064  pntibndlem3  27095  pntlem3  27112  ostthlem1  27130  ostthlem2  27131  sltres  27165  nogt01o  27199  oldbdayim  27383  addsproplem2  27454  negsproplem2  27503  mulsval  27565  idmot  27788  brcgr  28158  brbtwn2  28163  axsegconlem8  28182  axpaschlem  28198  axeuclid  28221  axcontlem2  28223  axcontlem7  28228  eengtrkg  28244  upgrex  28352  subgrprop3  28533  subupgr  28544  nbgr0vtxlem  28612  nb3grprlem1  28637  cusgredg  28681  cusgrres  28705  usgredgsscusgredg  28716  finsumvtxdg2ssteplem4  28805  finsumvtxdg2sstep  28806  wlkl1loop  28895  wlkp1lem4  28933  wwlksnred  29146  wwlksnext  29147  wwlksnextwrd  29151  wpthswwlks2on  29215  clwwlknp  29290  clwwlkel  29299  wwlksext2clwwlk  29310  clwwlknonwwlknonb  29359  3wlkond  29424  1conngr  29447  eucrctshift  29496  fusgr2wsp2nb  29587  numclwwlk1lem2foa  29607  numclwwlk1lem2f1  29610  numclwlk1lem1  29622  numclwlk1lem2  29623  grpoidinvlem1  29757  grporcan  29771  ipblnfi  30108  hvmulcan2  30326  shscli  30570  spansneleq  30823  pjspansn  30830  3oalem2  30916  eigposi  31089  cnlnadjlem2  31321  stlesi  31494  mdslmd1lem1  31578  mdslmd1lem2  31579  cdj1i  31686  disjxpin  31819  nn0xmulclb  31984  xreceu  32088  txomap  32814  pstmxmet  32877  qqhghm  32968  qqhrhm  32969  measinblem  33218  cntmeas  33224  ballotlemsf1o  33512  bnj945  33784  bnj1110  33993  f1resveqaeq  34088  cvmopnlem  34269  cvmfolem  34270  cvmliftmolem2  34273  cvmlift2lem10  34303  satf00  34365  satffunlem2lem1  34395  satefvfmla0  34409  mrsubvrs  34513  wzel  34796  btwnconn1lem8  35066  btwnconn1lem9  35067  btwnconn1lem10  35068  btwnconn1lem11  35069  btwnconn1lem12  35070  gg-dvcobr  35176  finminlem  35203  nn0prpwlem  35207  fnessref  35242  refssfne  35243  fnemeet2  35252  consym1  35305  bj-finsumval0  36166  topdifinffinlem  36228  relowlssretop  36244  rdgeqoa  36251  fvineqsneu  36292  pibt2  36298  matunitlindflem1  36484  poimirlem28  36516  mblfinlem1  36525  mblfinlem3  36527  mblfinlem4  36528  ovoliunnfl  36530  mbfresfi  36534  mbfposadd  36535  itg2addnclem2  36540  itg2addnc  36542  ftc1anc  36569  frinfm  36603  fdc  36613  blssp  36624  sstotbnd  36643  isbnd2  36651  ssbnd  36656  prdstotbnd  36662  prdsbnd2  36663  ismtyres  36676  heibor1lem  36677  rrnequiv  36703  rngoisocnv  36849  crngohomfo  36874  pridlc3  36941  membpartlem19  37681  prter3  37752  ax12eq  37811  ax12el  37812  cvratlem  38292  islvol2aN  38463  4atlem4b  38471  4atlem4c  38472  4atlem4d  38473  isline2  38645  isline3  38647  pclfinclN  38821  linepsubclN  38822  pexmidlem4N  38844  diaglbN  39926  dvhvaddcl  39966  dvhvaddcomN  39967  dvhvscacl  39974  djavalN  40006  dibglbN  40037  dihatexv  40209  djhval  40269  mapdrvallem2  40516  metakunt15  40999  evlselvlem  41158  evlselv  41159  mhpind  41166  prjsprellsp  41353  elrfi  41432  nacsfix  41450  eldioph2  41500  lzenom  41508  rexrabdioph  41532  irrapxlem3  41562  pellexlem5  41571  pellex  41573  pell1234qrne0  41591  pell1234qrmulcl  41593  pell14qrdich  41607  pell1qrge1  41608  pellqrex  41617  rmxypairf1o  41650  rmxycomplete  41656  monotoddzzfi  41681  congadd  41705  jm2.19lem3  41730  jm2.19lem4  41731  jm2.25  41738  jm2.26a  41739  jm2.26lem3  41740  expdiophlem1  41760  wepwsolem  41784  lmhmfgsplit  41828  aaitgo  41904  mon1psubm  41948  deg1mhm  41949  succlg  42078  ofoacom  42111  iunrelexp0  42453  isotone2  42800  mnuprdlem4  43034  disjrnmpt2  43886  mullimc  44332  mullimcf  44339  climxrre  44466  fprodcncf  44616  stoweidlem17  44733  stoweidlem27  44743  stoweidlem54  44770  fourierdlem42  44865  fourierdlem62  44884  fourierdlem73  44895  fourierdlem76  44898  fourierdlem97  44919  sge0iunmptlemfi  45129  isomenndlem  45246  imarnf1pr  45990  smonoord  46039  fvelsetpreimafv  46055  iccpartiltu  46090  sprsymrelf1lem  46159  prproropf1olem3  46173  paireqne  46179  fmtnoprmfac1  46233  prmdvdsfmtnof1lem2  46253  isomushgr  46494  isomuspgrlem2c  46498  mgmhmlin  46556  rnghmmul  46698  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  funcringcsetcALTV2lem9  46942  ringcinvALTV  46954  funcringcsetclem9ALTV  46965  mndpsuppss  47047  lmodvsmdi  47058  lincsum  47110  lindslinindimp2lem4  47142  nn0sumshdiglemB  47306  1arymaptf1  47328  2arymaptf1  47339