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  773  simprrl  781  simprrr  782  simprr1  1222  simprr2  1223  simprr3  1224  prneimg  4854  prproe  4905  fr2nr  5662  wereu2  5682  f1oprg  6893  fvtp1g  7218  funfvima3  7256  isof1oidb  7344  isomin  7357  weniso  7374  elovmpt3rab1  7693  sorpssi  7749  resf1extb  7956  poseq  8183  suppofssd  8228  tfrlem9a  8426  oalimcl  8598  odi  8617  oeeui  8640  ralxpmap  8936  boxriin  8980  domdifsn  9094  domunsncan  9112  enfixsn  9121  disjen  9174  mapen  9181  mapxpen  9183  mapunen  9186  findcard2d  9206  unxpdomlem2  9287  unxpdomlem3  9288  findcard3OLD  9319  isfinite2  9334  marypha1lem  9473  marypha2  9479  supmo  9492  infmo  9535  card2inf  9595  brwdom2  9613  wemapwe  9737  rankonidlem  9868  rankxplim3  9921  djulf1o  9952  djurf1o  9953  infxpenlem  10053  infxpenc2lem1  10059  infxpenc2  10062  fseqenlem1  10064  fseqenlem2  10065  infpwfien  10102  dfac12lem2  10185  infunsdom1  10252  infunsdom  10253  infmap2  10257  fin2i2  10358  fin23lem28  10380  fin23lem32  10384  fin23lem34  10386  fin23lem40  10391  isf32lem2  10394  compssiso  10414  isfin1-3  10426  fin1a2lem10  10449  fin12  10453  hsmexlem4  10469  ac6num  10519  ttukeylem7  10555  axdclem2  10560  iundom2g  10580  fpwwe2lem11  10681  pwfseqlem3  10700  winalim2  10736  winafp  10737  wunex2  10778  grur1  10860  dedekindle  11425  00id  11436  receu  11908  lt2mul2div  12146  peano5uzi  12707  uzwo  12953  qbtwnre  13241  iooshf  13466  modmul1  13965  seqcl2  14061  seqfveq2  14065  seqid2  14089  seqdistr  14094  expcl2lem  14114  mulexpz  14143  expnlbnd2  14273  hashfun  14476  hashfacen  14493  hashf1lem1  14494  elss2prb  14527  fstwrdne0  14594  swrdsb0eq  14701  swrdswrd  14743  wrd2ind  14761  swrdccatin1  14763  pfxccatin12  14771  splid  14791  repswrevw  14825  cshwidxmod  14841  cshwidx0  14844  2cshw  14851  cshweqrep  14859  cshw1  14860  wwlktovfo  14997  relexpfld  15088  relexpindlem  15102  01sqrexlem6  15286  absexpz  15344  o1rlimmul  15655  iseralt  15721  summolem2  15752  fsumf1o  15759  fsum0diag2  15819  fsummulc2  15820  cvgcmpce  15854  incexclem  15872  prodmolem2  15971  fprodcl2lem  15986  fprodmul  15996  fprodrev  16013  moddvds  16301  dvdsflip  16354  bitsf1ocnv  16481  sadcaddlem  16494  bezoutlem2  16577  bezoutlem4  16579  dfgcd2  16583  lcmgcdlem  16643  crth  16815  hashgcdlem  16825  phisum  16828  pcqcl  16894  pcid  16911  pcneg  16912  prmpwdvds  16942  pockthg  16944  4sqlem11  16993  ramub2  17052  0ram  17058  prmgaplem7  17095  prmgaplem8  17096  setscom  17217  qusval  17587  initoeu1  18056  termoeu1  18063  setcinv  18135  funcestrcsetclem9  18193  funcsetcestrclem9  18208  fullsetcestrc  18211  1stfcl  18242  2ndfcl  18243  hofpropd  18312  isacs3lem  18587  mgmhmlin  18712  mndpsuppss  18778  frmdss2  18876  frmdup1  18877  mgm2nsgrplem2  18932  mulgdirlem  19123  mulgass  19129  0nsg  19187  cycsubgcl  19224  ghmmulg  19246  conjghm  19267  qusghm  19273  gsumwrev  19385  symg2bas  19410  symgfixelsi  19453  f1otrspeq  19465  psgnunilem2  19513  psgnunilem3  19514  odf1o2  19591  lsmhash  19723  efgtf  19740  efginvrel2  19745  efgredeu  19770  efgcpbllemb  19773  frgpuplem  19790  frgpup1  19793  ghmcyg  19914  gsumval3lem1  19923  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumconst  19952  gsumzmhm  19955  gsumzoppg  19962  gsum2d  19990  subgdmdprd  20054  pgpfac1lem3  20097  gsummgp0  20315  rnghmmul  20449  rngcinv  20637  ringcinv  20671  islmodd  20864  lmodvsmmulgdi  20895  islss3  20957  0lmhm  21039  idlmhm  21040  lmhmeql  21054  pwssplit3  21060  lidldvgen  21344  qsssubdrg  21444  cnsubrg  21445  znf1o  21570  psgnghm  21598  psgndif  21620  cssmre  21711  dsmmsubg  21763  frlmup1  21818  lindfrn  21841  f1lindf  21842  evlslem1  22106  psdmul  22170  coe1tmmul2  22279  pf1ind  22359  mamufval  22396  mamurid  22448  mvmulfval  22548  mdetralt2  22615  mndifsplit  22642  maducoeval2  22646  madugsum  22649  mat2pmatmul  22737  decpmatmul  22778  pm2mpf1lem  22800  pm2mpf1  22805  monmat2matmon  22830  chpscmat  22848  fvmptnn04if  22855  tgcl  22976  ppttop  23014  epttop  23016  clsval2  23058  opncldf1  23092  mretopd  23100  neindisj  23125  neiptopnei  23140  restcls  23189  restntr  23190  ordtbas  23200  cnpnei  23272  cncls2  23281  tgcmp  23409  cmpcld  23410  uncmp  23411  hauscmplem  23414  1stcfb  23453  2ndcctbss  23463  hauspwdom  23509  reftr  23522  comppfsc  23540  kgentopon  23546  ptpjpre1  23579  ptcnplem  23629  txcn  23634  txdis1cn  23643  txhaus  23655  xkopt  23663  imasnopn  23698  imasncld  23699  imasncls  23700  hmeoimaf1o  23778  cmphaushmeo  23808  txhmeo  23811  trfbas2  23851  fbasfip  23876  fbasrn  23892  fmss  23954  elfm2  23956  hauspwpwf1  23995  flfcnp  24012  fclscf  24033  flimfnfcls  24036  fcfval  24041  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  ptcmplem3  24062  ptcmplem4  24063  cnextfval  24070  cnextcn  24075  tmdgsum2  24104  ustex2sym  24225  neipcfilu  24305  imasdsf1olem  24383  metss2lem  24524  stdbdxmet  24528  stdbdmopn  24531  metrest  24537  metcnp  24554  restmetu  24583  tngngp  24675  icccmplem1  24844  icccvx  24981  evth  24991  lebnumlem1  24993  pi1blem  25072  isncvsngp  25183  equivcau  25334  bcthlem5  25362  cmslssbn  25406  ivthlem3  25488  ovolicc2lem3  25554  ovolicc2lem4  25555  dyaddisj  25631  dyadmbllem  25634  ismbfd  25674  itg2seq  25777  itgss  25847  limciun  25929  dvcobr  25983  dvcobrOLD  25984  dvmptfsum  26013  c1liplem1  26035  c1lip1  26036  lhop  26055  dvcvx  26059  tdeglem4  26099  plyco0  26231  elply2  26235  plypf1  26251  dgreq0  26305  elqaalem2  26362  aalioulem6  26379  aaliou  26380  aaliou2b  26383  ulmss  26440  ulmcn  26442  pserulm  26465  lgamgulmlem5  27076  basellem4  27127  fsumdvdsdiaglem  27226  mpodvdsmulf1o  27237  dvdsmulf1o  27239  chtublem  27255  fsumvma2  27258  logfaclbnd  27266  dchrelbasd  27283  lgsqrlem2  27391  gausslemma2dlem1a  27409  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  rplogsumlem2  27529  rpvmasumlem  27531  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  rpvmasum2  27556  dchrisum0lem1  27560  logsqvma  27586  selberg4  27605  pntibndlem3  27636  pntlem3  27653  ostthlem1  27671  ostthlem2  27672  sltres  27707  nogt01o  27741  oldbdayim  27927  addsproplem2  28003  negsproplem2  28061  mulsval  28135  om2noseqrdg  28310  noseqrdgfn  28312  zmulscld  28383  recut  28428  idmot  28545  brcgr  28915  brbtwn2  28920  axsegconlem8  28939  axpaschlem  28955  axeuclid  28978  axcontlem2  28980  axcontlem7  28985  eengtrkg  29001  upgrex  29109  subgrprop3  29293  subupgr  29304  nbgr0edglem  29373  nb3grprlem1  29397  cusgredg  29441  cusgrres  29466  usgredgsscusgredg  29477  finsumvtxdg2ssteplem4  29566  finsumvtxdg2sstep  29567  wlkl1loop  29656  wlkp1lem4  29694  wwlksnred  29912  wwlksnext  29913  wwlksnextwrd  29917  wpthswwlks2on  29981  clwwlknp  30056  clwwlkel  30065  wwlksext2clwwlk  30076  clwwlknonwwlknonb  30125  3wlkond  30190  1conngr  30213  eucrctshift  30262  fusgr2wsp2nb  30353  numclwwlk1lem2foa  30373  numclwwlk1lem2f1  30376  numclwlk1lem1  30388  numclwlk1lem2  30389  grpoidinvlem1  30523  grporcan  30537  ipblnfi  30874  hvmulcan2  31092  shscli  31336  spansneleq  31589  pjspansn  31596  3oalem2  31682  eigposi  31855  cnlnadjlem2  32087  stlesi  32260  mdslmd1lem1  32344  mdslmd1lem2  32345  cdj1i  32452  disjxpin  32601  nn0xmulclb  32775  xreceu  32904  txomap  33833  pstmxmet  33896  qqhghm  33989  qqhrhm  33990  measinblem  34221  cntmeas  34227  ballotlemsf1o  34516  bnj945  34787  bnj1110  34996  f1resveqaeq  35099  cvmopnlem  35283  cvmfolem  35284  cvmliftmolem2  35287  cvmlift2lem10  35317  satf00  35379  satffunlem2lem1  35409  satefvfmla0  35423  mrsubvrs  35527  wzel  35825  btwnconn1lem8  36095  btwnconn1lem9  36096  btwnconn1lem10  36097  btwnconn1lem11  36098  btwnconn1lem12  36099  finminlem  36319  nn0prpwlem  36323  fnessref  36358  refssfne  36359  fnemeet2  36368  consym1  36421  bj-finsumval0  37286  topdifinffinlem  37348  relowlssretop  37364  rdgeqoa  37371  fvineqsneu  37412  pibt2  37418  matunitlindflem1  37623  poimirlem28  37655  mblfinlem1  37664  mblfinlem3  37666  mblfinlem4  37667  ovoliunnfl  37669  mbfresfi  37673  mbfposadd  37674  itg2addnclem2  37679  itg2addnc  37681  ftc1anc  37708  frinfm  37742  fdc  37752  blssp  37763  sstotbnd  37782  isbnd2  37790  ssbnd  37795  prdstotbnd  37801  prdsbnd2  37802  ismtyres  37815  heibor1lem  37816  rrnequiv  37842  rngoisocnv  37988  crngohomfo  38013  pridlc3  38080  membpartlem19  38812  prter3  38883  ax12eq  38942  ax12el  38943  cvratlem  39423  islvol2aN  39594  4atlem4b  39602  4atlem4c  39603  4atlem4d  39604  isline2  39776  isline3  39778  pclfinclN  39952  linepsubclN  39953  pexmidlem4N  39975  diaglbN  41057  dvhvaddcl  41097  dvhvaddcomN  41098  dvhvscacl  41105  djavalN  41137  dibglbN  41168  dihatexv  41340  djhval  41400  mapdrvallem2  41647  metakunt15  42220  evlselvlem  42596  evlselv  42597  mhpind  42604  prjsprellsp  42621  elrfi  42705  nacsfix  42723  eldioph2  42773  lzenom  42781  rexrabdioph  42805  irrapxlem3  42835  pellexlem5  42844  pellex  42846  pell1234qrne0  42864  pell1234qrmulcl  42866  pell14qrdich  42880  pell1qrge1  42881  pellqrex  42890  rmxypairf1o  42923  rmxycomplete  42929  monotoddzzfi  42954  congadd  42978  jm2.19lem3  43003  jm2.19lem4  43004  jm2.25  43011  jm2.26a  43012  jm2.26lem3  43013  expdiophlem1  43033  wepwsolem  43054  lmhmfgsplit  43098  aaitgo  43174  mon1psubm  43211  deg1mhm  43212  succlg  43341  ofoacom  43374  iunrelexp0  43715  isotone2  44062  mnuprdlem4  44294  relpmin  44973  disjrnmpt2  45193  mullimc  45631  mullimcf  45638  climxrre  45765  fprodcncf  45915  stoweidlem17  46032  stoweidlem27  46042  stoweidlem54  46069  fourierdlem42  46164  fourierdlem62  46183  fourierdlem73  46194  fourierdlem76  46197  fourierdlem97  46218  sge0iunmptlemfi  46428  isomenndlem  46545  imarnf1pr  47294  smonoord  47358  fvelsetpreimafv  47374  iccpartiltu  47409  sprsymrelf1lem  47478  prproropf1olem3  47492  paireqne  47498  fmtnoprmfac1  47552  prmdvdsfmtnof1lem2  47572  uspgrimprop  47873  gricushgr  47886  grimedg  47903  cycl3grtri  47914  rngcinvALTV  48192  funcringcsetcALTV2lem9  48214  ringcinvALTV  48226  funcringcsetclem9ALTV  48237  lmodvsmdi  48295  lincsum  48346  lindslinindimp2lem4  48378  nn0sumshdiglemB  48541  1arymaptf1  48563  2arymaptf1  48574  oduoppcciso  49170