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  4814  prproe  4865  fr2nr  5608  wereu2  5628  f1oprg  6827  fvtp1g  7154  funfvima3  7192  isof1oidb  7281  isomin  7294  weniso  7311  elovmpt3rab1  7629  sorpssi  7685  resf1extb  7890  poseq  8114  suppofssd  8159  tfrlem9a  8331  oalimcl  8501  odi  8520  oeeui  8543  ralxpmap  8846  boxriin  8890  domdifsn  9001  domunsncan  9018  enfixsn  9027  disjen  9075  mapen  9082  mapxpen  9084  mapunen  9087  findcard2d  9107  unxpdomlem2  9174  unxpdomlem3  9175  findcard3OLD  9206  isfinite2  9221  marypha1lem  9360  marypha2  9366  supmo  9379  infmo  9424  card2inf  9484  brwdom2  9502  wemapwe  9626  rankonidlem  9757  rankxplim3  9810  djulf1o  9841  djurf1o  9842  infxpenlem  9942  infxpenc2lem1  9948  infxpenc2  9951  fseqenlem1  9953  fseqenlem2  9954  infpwfien  9991  dfac12lem2  10074  infunsdom1  10141  infunsdom  10142  infmap2  10146  fin2i2  10247  fin23lem28  10269  fin23lem32  10273  fin23lem34  10275  fin23lem40  10280  isf32lem2  10283  compssiso  10303  isfin1-3  10315  fin1a2lem10  10338  fin12  10342  hsmexlem4  10358  ac6num  10408  ttukeylem7  10444  axdclem2  10449  iundom2g  10469  fpwwe2lem11  10570  pwfseqlem3  10589  winalim2  10625  winafp  10626  wunex2  10667  grur1  10749  dedekindle  11314  00id  11325  receu  11799  lt2mul2div  12037  peano5uzi  12599  uzwo  12846  qbtwnre  13135  iooshf  13363  modmul1  13865  seqcl2  13961  seqfveq2  13965  seqid2  13989  seqdistr  13994  expcl2lem  14014  mulexpz  14043  expnlbnd2  14175  hashfun  14378  hashfacen  14395  hashf1lem1  14396  elss2prb  14429  fstwrdne0  14497  swrdsb0eq  14604  swrdswrd  14646  wrd2ind  14664  swrdccatin1  14666  pfxccatin12  14674  splid  14694  repswrevw  14728  cshwidxmod  14744  cshwidx0  14747  2cshw  14754  cshweqrep  14762  cshw1  14763  wwlktovfo  14900  relexpfld  14991  relexpindlem  15005  01sqrexlem6  15189  absexpz  15247  o1rlimmul  15561  iseralt  15627  summolem2  15658  fsumf1o  15665  fsum0diag2  15725  fsummulc2  15726  cvgcmpce  15760  incexclem  15778  prodmolem2  15877  fprodcl2lem  15892  fprodmul  15902  fprodrev  15919  moddvds  16209  dvdsflip  16263  bitsf1ocnv  16390  sadcaddlem  16403  bezoutlem2  16486  bezoutlem4  16488  dfgcd2  16492  lcmgcdlem  16552  crth  16724  hashgcdlem  16734  phisum  16737  pcqcl  16803  pcid  16820  pcneg  16821  prmpwdvds  16851  pockthg  16853  4sqlem11  16902  ramub2  16961  0ram  16967  prmgaplem7  17004  prmgaplem8  17005  setscom  17126  qusval  17481  initoeu1  17953  termoeu1  17960  setcinv  18032  funcestrcsetclem9  18089  funcsetcestrclem9  18104  fullsetcestrc  18107  1stfcl  18138  2ndfcl  18139  hofpropd  18208  isacs3lem  18483  mgmhmlin  18608  mndpsuppss  18674  frmdss2  18772  frmdup1  18773  mgm2nsgrplem2  18828  mulgdirlem  19019  mulgass  19025  0nsg  19083  cycsubgcl  19120  ghmmulg  19142  conjghm  19163  qusghm  19169  gsumwrev  19280  symg2bas  19307  symgfixelsi  19349  f1otrspeq  19361  psgnunilem2  19409  psgnunilem3  19410  odf1o2  19487  lsmhash  19619  efgtf  19636  efginvrel2  19641  efgredeu  19666  efgcpbllemb  19669  frgpuplem  19686  frgpup1  19689  ghmcyg  19810  gsumval3lem1  19819  gsumzres  19823  gsumzcl2  19824  gsumzf1o  19826  gsumzaddlem  19835  gsumconst  19848  gsumzmhm  19851  gsumzoppg  19858  gsum2d  19886  subgdmdprd  19950  pgpfac1lem3  19993  gsummgp0  20238  rnghmmul  20369  rngcinv  20557  ringcinv  20591  islmodd  20804  lmodvsmmulgdi  20835  islss3  20897  0lmhm  20979  idlmhm  20980  lmhmeql  20994  pwssplit3  21000  lidldvgen  21276  qsssubdrg  21368  cnsubrg  21369  znf1o  21493  psgnghm  21522  psgndif  21544  cssmre  21635  dsmmsubg  21685  frlmup1  21740  lindfrn  21763  f1lindf  21764  evlslem1  22022  psdmul  22086  coe1tmmul2  22195  pf1ind  22275  mamufval  22312  mamurid  22362  mvmulfval  22462  mdetralt2  22529  mndifsplit  22556  maducoeval2  22560  madugsum  22563  mat2pmatmul  22651  decpmatmul  22692  pm2mpf1lem  22714  pm2mpf1  22719  monmat2matmon  22744  chpscmat  22762  fvmptnn04if  22769  tgcl  22889  ppttop  22927  epttop  22929  clsval2  22970  opncldf1  23004  mretopd  23012  neindisj  23037  neiptopnei  23052  restcls  23101  restntr  23102  ordtbas  23112  cnpnei  23184  cncls2  23193  tgcmp  23321  cmpcld  23322  uncmp  23323  hauscmplem  23326  1stcfb  23365  2ndcctbss  23375  hauspwdom  23421  reftr  23434  comppfsc  23452  kgentopon  23458  ptpjpre1  23491  ptcnplem  23541  txcn  23546  txdis1cn  23555  txhaus  23567  xkopt  23575  imasnopn  23610  imasncld  23611  imasncls  23612  hmeoimaf1o  23690  cmphaushmeo  23720  txhmeo  23723  trfbas2  23763  fbasfip  23788  fbasrn  23804  fmss  23866  elfm2  23868  hauspwpwf1  23907  flfcnp  23924  fclscf  23945  flimfnfcls  23948  fcfval  23953  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALTlem4  23970  ptcmplem3  23974  ptcmplem4  23975  cnextfval  23982  cnextcn  23987  tmdgsum2  24016  ustex2sym  24137  neipcfilu  24216  imasdsf1olem  24294  metss2lem  24432  stdbdxmet  24436  stdbdmopn  24439  metrest  24445  metcnp  24462  restmetu  24491  tngngp  24575  icccmplem1  24744  icccvx  24881  evth  24891  lebnumlem1  24893  pi1blem  24972  isncvsngp  25082  equivcau  25233  bcthlem5  25261  cmslssbn  25305  ivthlem3  25387  ovolicc2lem3  25453  ovolicc2lem4  25454  dyaddisj  25530  dyadmbllem  25533  ismbfd  25573  itg2seq  25676  itgss  25746  limciun  25828  dvcobr  25882  dvcobrOLD  25883  dvmptfsum  25912  c1liplem1  25934  c1lip1  25935  lhop  25954  dvcvx  25958  tdeglem4  25998  plyco0  26130  elply2  26134  plypf1  26150  dgreq0  26204  elqaalem2  26261  aalioulem6  26278  aaliou  26279  aaliou2b  26282  ulmss  26339  ulmcn  26341  pserulm  26364  lgamgulmlem5  26976  basellem4  27027  fsumdvdsdiaglem  27126  mpodvdsmulf1o  27137  dvdsmulf1o  27139  chtublem  27155  fsumvma2  27158  logfaclbnd  27166  dchrelbasd  27183  lgsqrlem2  27291  gausslemma2dlem1a  27309  lgseisenlem2  27320  lgsquadlem1  27324  lgsquadlem2  27325  lgsquadlem3  27326  rplogsumlem2  27429  rpvmasumlem  27431  dchrmusum2  27438  dchrvmasumlem1  27439  dchrvmasum2lem  27440  rpvmasum2  27456  dchrisum0lem1  27460  logsqvma  27486  selberg4  27505  pntibndlem3  27536  pntlem3  27553  ostthlem1  27571  ostthlem2  27572  sltres  27607  nogt01o  27641  oldbdayim  27838  addsproplem2  27917  negsproplem2  27975  mulsval  28052  om2noseqrdg  28238  noseqrdgfn  28240  zmulscld  28325  recut  28400  idmot  28517  brcgr  28880  brbtwn2  28885  axsegconlem8  28904  axpaschlem  28920  axeuclid  28943  axcontlem2  28945  axcontlem7  28950  eengtrkg  28966  upgrex  29072  subgrprop3  29256  subupgr  29267  nbgr0edglem  29336  nb3grprlem1  29360  cusgredg  29404  cusgrres  29429  usgredgsscusgredg  29440  finsumvtxdg2ssteplem4  29529  finsumvtxdg2sstep  29530  wlkl1loop  29618  wlkp1lem4  29655  wwlksnred  29872  wwlksnext  29873  wwlksnextwrd  29877  wpthswwlks2on  29941  clwwlknp  30016  clwwlkel  30025  wwlksext2clwwlk  30036  clwwlknonwwlknonb  30085  3wlkond  30150  1conngr  30173  eucrctshift  30222  fusgr2wsp2nb  30313  numclwwlk1lem2foa  30333  numclwwlk1lem2f1  30336  numclwlk1lem1  30348  numclwlk1lem2  30349  grpoidinvlem1  30483  grporcan  30497  ipblnfi  30834  hvmulcan2  31052  shscli  31296  spansneleq  31549  pjspansn  31556  3oalem2  31642  eigposi  31815  cnlnadjlem2  32047  stlesi  32220  mdslmd1lem1  32304  mdslmd1lem2  32305  cdj1i  32412  disjxpin  32567  nn0xmulclb  32744  xreceu  32892  txomap  33817  pstmxmet  33880  qqhghm  33971  qqhrhm  33972  measinblem  34203  cntmeas  34209  ballotlemsf1o  34498  bnj945  34756  bnj1110  34965  f1resveqaeq  35068  cvmopnlem  35258  cvmfolem  35259  cvmliftmolem2  35262  cvmlift2lem10  35292  satf00  35354  satffunlem2lem1  35384  satefvfmla0  35398  mrsubvrs  35502  wzel  35805  btwnconn1lem8  36075  btwnconn1lem9  36076  btwnconn1lem10  36077  btwnconn1lem11  36078  btwnconn1lem12  36079  finminlem  36299  nn0prpwlem  36303  fnessref  36338  refssfne  36339  fnemeet2  36348  consym1  36401  bj-finsumval0  37266  topdifinffinlem  37328  relowlssretop  37344  rdgeqoa  37351  fvineqsneu  37392  pibt2  37398  matunitlindflem1  37603  poimirlem28  37635  mblfinlem1  37644  mblfinlem3  37646  mblfinlem4  37647  ovoliunnfl  37649  mbfresfi  37653  mbfposadd  37654  itg2addnclem2  37659  itg2addnc  37661  ftc1anc  37688  frinfm  37722  fdc  37732  blssp  37743  sstotbnd  37762  isbnd2  37770  ssbnd  37775  prdstotbnd  37781  prdsbnd2  37782  ismtyres  37795  heibor1lem  37796  rrnequiv  37822  rngoisocnv  37968  crngohomfo  37993  pridlc3  38060  membpartlem19  38796  prter3  38868  ax12eq  38927  ax12el  38928  cvratlem  39408  islvol2aN  39579  4atlem4b  39587  4atlem4c  39588  4atlem4d  39589  isline2  39761  isline3  39763  pclfinclN  39937  linepsubclN  39938  pexmidlem4N  39960  diaglbN  41042  dvhvaddcl  41082  dvhvaddcomN  41083  dvhvscacl  41090  djavalN  41122  dibglbN  41153  dihatexv  41325  djhval  41385  mapdrvallem2  41632  evlselvlem  42567  evlselv  42568  mhpind  42575  prjsprellsp  42592  elrfi  42675  nacsfix  42693  eldioph2  42743  lzenom  42751  rexrabdioph  42775  irrapxlem3  42805  pellexlem5  42814  pellex  42816  pell1234qrne0  42834  pell1234qrmulcl  42836  pell14qrdich  42850  pell1qrge1  42851  pellqrex  42860  rmxypairf1o  42893  rmxycomplete  42899  monotoddzzfi  42924  congadd  42948  jm2.19lem3  42973  jm2.19lem4  42974  jm2.25  42981  jm2.26a  42982  jm2.26lem3  42983  expdiophlem1  43003  wepwsolem  43024  lmhmfgsplit  43068  aaitgo  43144  mon1psubm  43181  deg1mhm  43182  succlg  43310  ofoacom  43343  iunrelexp0  43684  isotone2  44031  mnuprdlem4  44257  relpmin  44935  disjrnmpt2  45175  mullimc  45607  mullimcf  45614  climxrre  45741  fprodcncf  45891  stoweidlem17  46008  stoweidlem27  46018  stoweidlem54  46045  fourierdlem42  46140  fourierdlem62  46159  fourierdlem73  46170  fourierdlem76  46173  fourierdlem97  46194  sge0iunmptlemfi  46404  isomenndlem  46521  imarnf1pr  47276  smonoord  47365  fvelsetpreimafv  47381  iccpartiltu  47416  sprsymrelf1lem  47485  prproropf1olem3  47499  paireqne  47505  fmtnoprmfac1  47559  prmdvdsfmtnof1lem2  47579  gricushgr  47910  grimedg  47928  cycl3grtri  47939  gpgedg2iv  48051  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  rngcinvALTV  48257  funcringcsetcALTV2lem9  48279  ringcinvALTV  48291  funcringcsetclem9ALTV  48302  lmodvsmdi  48360  lincsum  48411  lindslinindimp2lem4  48443  nn0sumshdiglemB  48602  1arymaptf1  48624  2arymaptf1  48635  dmrnxp  48818  xpco2  48838  initopropd  49225  termopropd  49226  zeroopropd  49227  oduoppcciso  49548  lanpropd  49597  ranpropd  49598