Theorem ad2antll 725

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

This theorem is referenced by:  simprr  769  simprrl  777  simprrr  778  simprr1  1219  simprr2  1220  simprr3  1221  prneimg  4782  fr2nr  5558  wereu2  5577  f1oprg  6744  fvtp1g  7055  funfvima3  7094  isof1oidb  7175  isomin  7188  weniso  7205  elovmpt3rab1  7507  sorpssi  7560  suppofssd  7990  tfrlem9a  8188  oalimcl  8353  odi  8372  oeeui  8395  ralxpmap  8642  boxriin  8686  domdifsn  8795  domunsncan  8812  enfixsn  8821  disjen  8870  mapen  8877  mapxpen  8879  mapunen  8882  findcard2d  8911  unxpdomlem2  8957  unxpdomlem3  8958  findcard3  8987  isfinite2  9002  marypha1lem  9122  marypha2  9128  supmo  9141  infmo  9184  card2inf  9244  brwdom2  9262  wemapwe  9385  rankonidlem  9517  rankxplim3  9570  djulf1o  9601  djurf1o  9602  infxpenlem  9700  infxpenc2lem1  9706  infxpenc2  9709  fseqenlem1  9711  fseqenlem2  9712  infpwfien  9749  dfac12lem2  9831  infunsdom1  9900  infunsdom  9901  infmap2  9905  fin2i2  10005  fin23lem28  10027  fin23lem32  10031  fin23lem34  10033  fin23lem40  10038  isf32lem2  10041  compssiso  10061  isfin1-3  10073  fin1a2lem10  10096  fin12  10100  hsmexlem4  10116  ac6num  10166  ttukeylem7  10202  axdclem2  10207  iundom2g  10227  fpwwe2lem11  10328  pwfseqlem3  10347  winalim2  10383  winafp  10384  wunex2  10425  grur1  10507  dedekindle  11069  00id  11080  receu  11550  lt2mul2div  11783  peano5uzi  12339  uzwo  12580  qbtwnre  12862  iooshf  13087  modmul1  13572  seqcl2  13669  seqfveq2  13673  seqid2  13697  seqdistr  13702  expcl2lem  13722  mulexpz  13751  expnlbnd2  13877  hashfun  14080  hashfacen  14094  hashfacenOLD  14095  hashf1lem1  14096  hashf1lem1OLD  14097  elss2prb  14129  fstwrdne0  14187  swrdsb0eq  14304  swrdswrd  14346  wrd2ind  14364  swrdccatin1  14366  pfxccatin12  14374  splid  14394  repswrevw  14428  cshwidxmod  14444  cshwidx0  14447  2cshw  14454  cshweqrep  14462  cshw1  14463  wwlktovfo  14601  relexpfld  14688  relexpindlem  14702  sqrlem6  14887  absexpz  14945  o1rlimmul  15256  iseralt  15324  summolem2  15356  fsumf1o  15363  fsum0diag2  15423  fsummulc2  15424  cvgcmpce  15458  incexclem  15476  prodmolem2  15573  fprodcl2lem  15588  fprodmul  15598  fprodrev  15615  moddvds  15902  dvdsflip  15954  bitsf1ocnv  16079  sadcaddlem  16092  bezoutlem2  16176  bezoutlem4  16178  dfgcd2  16182  lcmgcdlem  16239  crth  16407  hashgcdlem  16417  phisum  16419  pcqcl  16485  pcid  16502  pcneg  16503  prmpwdvds  16533  pockthg  16535  4sqlem11  16584  ramub2  16643  0ram  16649  prmgaplem7  16686  prmgaplem8  16687  setscom  16809  qusval  17170  initoeu1  17642  termoeu1  17649  setcinv  17721  funcestrcsetclem9  17781  funcsetcestrclem9  17796  fullsetcestrc  17799  1stfcl  17830  2ndfcl  17831  hofpropd  17901  isacs3lem  18175  frmdss2  18417  frmdup1  18418  mgm2nsgrplem2  18473  mulgdirlem  18649  mulgass  18655  0nsg  18712  cycsubgcl  18740  ghmmulg  18761  conjghm  18780  qusghm  18786  gsumwrev  18888  symg2bas  18915  symgfixelsi  18958  f1otrspeq  18970  psgnunilem2  19018  psgnunilem3  19019  odf1o2  19093  lsmhash  19226  efgtf  19243  efginvrel2  19248  efgredeu  19273  efgcpbllemb  19276  frgpuplem  19293  frgpup1  19296  cygablOLD  19407  ghmcyg  19412  gsumval3lem1  19421  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  gsum2d  19488  subgdmdprd  19552  pgpfac1lem3  19595  gsummgp0  19762  islmodd  20044  lmodvsmmulgdi  20073  islss3  20136  0lmhm  20217  idlmhm  20218  lmhmeql  20232  pwssplit3  20238  lidldvgen  20439  qsssubdrg  20569  cnsubrg  20570  znf1o  20671  psgnghm  20697  psgndif  20719  cssmre  20810  dsmmsubg  20860  frlmup1  20915  lindfrn  20938  f1lindf  20939  evlslem1  21202  coe1tmmul2  21357  pf1ind  21431  mamufval  21444  mamurid  21499  mvmulfval  21599  mdetralt2  21666  mndifsplit  21693  maducoeval2  21697  madugsum  21700  mat2pmatmul  21788  decpmatmul  21829  pm2mpf1lem  21851  pm2mpf1  21856  monmat2matmon  21881  chpscmat  21899  fvmptnn04if  21906  tgcl  22027  ppttop  22065  epttop  22067  clsval2  22109  opncldf1  22143  mretopd  22151  neindisj  22176  neiptopnei  22191  restcls  22240  restntr  22241  ordtbas  22251  cnpnei  22323  cncls2  22332  tgcmp  22460  cmpcld  22461  uncmp  22462  hauscmplem  22465  1stcfb  22504  2ndcctbss  22514  hauspwdom  22560  reftr  22573  comppfsc  22591  kgentopon  22597  ptpjpre1  22630  ptcnplem  22680  txcn  22685  txdis1cn  22694  txhaus  22706  xkopt  22714  imasnopn  22749  imasncld  22750  imasncls  22751  hmeoimaf1o  22829  cmphaushmeo  22859  txhmeo  22862  trfbas2  22902  fbasfip  22927  fbasrn  22943  fmss  23005  elfm2  23007  hauspwpwf1  23046  flfcnp  23063  fclscf  23084  flimfnfcls  23087  fcfval  23092  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem3  23113  ptcmplem4  23114  cnextfval  23121  cnextcn  23126  tmdgsum2  23155  ustex2sym  23276  neipcfilu  23356  imasdsf1olem  23434  metss2lem  23573  stdbdxmet  23577  stdbdmopn  23580  metrest  23586  metcnp  23603  restmetu  23632  tngngp  23724  icccmplem1  23891  icccvx  24019  evth  24028  lebnumlem1  24030  pi1blem  24108  isncvsngp  24218  equivcau  24369  bcthlem5  24397  cmslssbn  24441  ivthlem3  24522  ovolicc2lem3  24588  ovolicc2lem4  24589  dyaddisj  24665  dyadmbllem  24668  ismbfd  24708  itg2seq  24812  itgss  24881  limciun  24963  dvcobr  25015  dvmptfsum  25044  c1liplem1  25065  c1lip1  25066  lhop  25085  dvcvx  25089  tdeglem4  25129  plyco0  25258  elply2  25262  plypf1  25278  dgreq0  25331  elqaalem2  25385  aalioulem6  25402  aaliou  25403  aaliou2b  25406  ulmss  25461  ulmcn  25463  pserulm  25486  lgamgulmlem5  26087  basellem4  26138  fsumdvdsdiaglem  26237  dvdsmulf1o  26248  chtublem  26264  fsumvma2  26267  logfaclbnd  26275  dchrelbasd  26292  lgsqrlem2  26400  gausslemma2dlem1a  26418  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  rplogsumlem2  26538  rpvmasumlem  26540  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  rpvmasum2  26565  dchrisum0lem1  26569  logsqvma  26595  selberg4  26614  pntibndlem3  26645  pntlem3  26662  ostthlem1  26680  ostthlem2  26681  idmot  26802  brcgr  27171  brbtwn2  27176  axsegconlem8  27195  axpaschlem  27211  axeuclid  27234  axcontlem2  27236  axcontlem7  27241  eengtrkg  27257  upgrex  27365  subgrprop3  27546  subupgr  27557  nbgr0vtxlem  27625  nb3grprlem1  27650  cusgredg  27694  cusgrres  27718  usgredgsscusgredg  27729  finsumvtxdg2ssteplem4  27818  finsumvtxdg2sstep  27819  wlkl1loop  27907  wlkp1lem4  27946  wwlksnred  28158  wwlksnext  28159  wwlksnextwrd  28163  wpthswwlks2on  28227  clwwlknp  28302  clwwlkel  28311  wwlksext2clwwlk  28322  clwwlknonwwlknonb  28371  3wlkond  28436  1conngr  28459  eucrctshift  28508  fusgr2wsp2nb  28599  numclwwlk1lem2foa  28619  numclwwlk1lem2f1  28622  numclwlk1lem1  28634  numclwlk1lem2  28635  grpoidinvlem1  28767  grporcan  28781  ipblnfi  29118  hvmulcan2  29336  shscli  29580  spansneleq  29833  pjspansn  29840  3oalem2  29926  eigposi  30099  cnlnadjlem2  30331  stlesi  30504  mdslmd1lem1  30588  mdslmd1lem2  30589  cdj1i  30696  disjxpin  30828  nn0xmulclb  30996  xreceu  31098  txomap  31686  pstmxmet  31749  qqhghm  31838  qqhrhm  31839  measinblem  32088  cntmeas  32094  ballotlemsf1o  32380  bnj945  32653  bnj1110  32862  f1resveqaeq  32957  cvmopnlem  33140  cvmfolem  33141  cvmliftmolem2  33144  cvmlift2lem10  33174  satf00  33236  satffunlem2lem1  33266  satefvfmla0  33280  mrsubvrs  33384  poxp3  33723  poseq  33729  wzel  33745  sltres  33792  nogt01o  33826  oldbdayim  33998  btwnconn1lem8  34323  btwnconn1lem9  34324  btwnconn1lem10  34325  btwnconn1lem11  34326  btwnconn1lem12  34327  finminlem  34434  nn0prpwlem  34438  fnessref  34473  refssfne  34474  fnemeet2  34483  consym1  34536  bj-finsumval0  35383  topdifinffinlem  35445  relowlssretop  35461  rdgeqoa  35468  fvineqsneu  35509  pibt2  35515  matunitlindflem1  35700  poimirlem28  35732  mblfinlem1  35741  mblfinlem3  35743  mblfinlem4  35744  ovoliunnfl  35746  mbfresfi  35750  mbfposadd  35751  itg2addnclem2  35756  itg2addnc  35758  ftc1anc  35785  frinfm  35820  fdc  35830  blssp  35841  sstotbnd  35860  isbnd2  35868  ssbnd  35873  prdstotbnd  35879  prdsbnd2  35880  ismtyres  35893  heibor1lem  35894  rrnequiv  35920  rngoisocnv  36066  crngohomfo  36091  pridlc3  36158  prter3  36823  ax12eq  36882  ax12el  36883  cvratlem  37362  islvol2aN  37533  4atlem4b  37541  4atlem4c  37542  4atlem4d  37543  isline2  37715  isline3  37717  pclfinclN  37891  linepsubclN  37892  pexmidlem4N  37914  diaglbN  38996  dvhvaddcl  39036  dvhvaddcomN  39037  dvhvscacl  39044  djavalN  39076  dibglbN  39107  dihatexv  39279  djhval  39339  mapdrvallem2  39586  metakunt15  40067  mhpind  40206  prjsprellsp  40371  elrfi  40432  nacsfix  40450  eldioph2  40500  lzenom  40508  rexrabdioph  40532  irrapxlem3  40562  pellexlem5  40571  pellex  40573  pell1234qrne0  40591  pell1234qrmulcl  40593  pell14qrdich  40607  pell1qrge1  40608  pellqrex  40617  rmxypairf1o  40649  rmxycomplete  40655  monotoddzzfi  40680  congadd  40704  jm2.19lem3  40729  jm2.19lem4  40730  jm2.25  40737  jm2.26a  40738  jm2.26lem3  40739  expdiophlem1  40759  wepwsolem  40783  lmhmfgsplit  40827  aaitgo  40903  mon1psubm  40947  deg1mhm  40948  iunrelexp0  41199  isotone2  41548  mnuprdlem4  41782  disjrnmpt2  42615  mullimc  43047  mullimcf  43054  climxrre  43181  fprodcncf  43331  stoweidlem17  43448  stoweidlem27  43458  stoweidlem54  43485  fourierdlem42  43580  fourierdlem62  43599  fourierdlem73  43610  fourierdlem76  43613  fourierdlem97  43634  sge0iunmptlemfi  43841  isomenndlem  43958  ovnsslelem  43988  imarnf1pr  44661  smonoord  44711  fvelsetpreimafv  44727  iccpartiltu  44762  sprsymrelf1lem  44831  prproropf1olem3  44845  paireqne  44851  fmtnoprmfac1  44905  prmdvdsfmtnof1lem2  44925  isomushgr  45166  isomuspgrlem2c  45170  mgmhmlin  45228  rnghmmul  45346  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  funcringcsetcALTV2lem9  45490  ringcinvALTV  45502  funcringcsetclem9ALTV  45513  mndpsuppss  45595  lmodvsmdi  45606  lincsum  45658  lindslinindimp2lem4  45690  nn0sumshdiglemB  45854  1arymaptf1  45876  2arymaptf1  45887