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  5632  wereu2  5652  f1oprg  6865  fvtp1g  7197  funfvima3  7236  f1resveqaeq  7271  isof1oidb  7326  isomin  7339  weniso  7358  elovmpt3rab1  7675  sorpssi  7731  resf1extb  7932  poseq  8157  suppofssd  8202  tfrlem9a  8376  oalimcl  8550  odi  8569  oeeui  8593  ralxpmap  8906  boxriin  8950  domdifsn  9061  domunsncan  9078  enfixsn  9087  disjen  9135  mapen  9142  mapxpen  9144  mapunen  9147  findcard2d  9164  unxpdomlem2  9230  unxpdomlem3  9231  isfinite2  9271  marypha1lem  9406  marypha2  9412  supmo  9425  infmo  9470  card2inf  9530  brwdom2  9548  wemapwe  9679  rankonidlem  9813  rankxplim3  9866  djulf1o  9920  djurf1o  9921  infxpenlem  10019  infxpenc2lem1  10025  infxpenc2  10028  fseqenlem1  10030  fseqenlem2  10031  infpwfien  10068  dfac12lem2  10150  infunsdom1  10217  infunsdom  10218  infmap2  10222  fin2i2  10323  fin23lem28  10345  fin23lem32  10349  fin23lem34  10351  fin23lem40  10356  isf32lem2  10359  compssiso  10379  isfin1-3  10391  fin1a2lem10  10414  fin12  10418  hsmexlem4  10434  ac6num  10484  ttukeylem7  10520  axdclem2  10525  iundom2g  10551  fpwwe2lem11  10653  pwfseqlem3  10672  winalim2  10708  winafp  10709  wunex2  10750  grur1  10832  dedekindle  11401  00id  11412  receu  11886  lt2mul2div  12120  peano5uzi  12713  uzwo  12963  qbtwnre  13254  iooshf  13482  modmul1  13991  seqcl2  14087  seqfveq2  14091  seqid2  14115  seqdistr  14120  expcl2lem  14140  mulexpz  14169  expnlbnd2  14301  hashfun  14505  hashfacen  14522  hashf1lem1  14523  elss2prb  14556  fstwrdne0  14624  swrdsb0eq  14736  swrdswrd  14777  wrd2ind  14795  swrdccatin1  14797  pfxccatin12  14805  splid  14825  repswrevw  14861  cshwidxmod  14877  cshwidx0  14880  2cshw  14887  cshweqrep  14895  cshw1  14896  wwlktovfo  15034  relexpfld  15125  relexpindlem  15139  01sqrexlem6  15337  absexpz  15395  o1rlimmul  15709  iseralt  15775  summolem2  15805  fsumf1o  15812  fsum0diag2  15872  fsummulc2  15873  cvgcmpce  15908  incexclem  15928  prodmolem2  16025  fprodcl2lem  16040  fprodmul  16050  fprodrev  16067  moddvds  16356  dvdsflip  16410  bitsf1ocnv  16537  sadcaddlem  16550  bezoutlem2  16633  bezoutlem4  16635  dfgcd2  16639  lcmgcdlem  16699  crth  16872  hashgcdlem  16882  phisum  16885  pcqcl  16951  pcid  16968  pcneg  16969  prmpwdvds  16999  pockthg  17001  4sqlem11  17050  ramub2  17109  0ram  17115  prmgaplem7  17152  prmgaplem8  17153  setscom  17275  qusval  17631  initoeu1  18103  termoeu1  18110  setcinv  18182  funcestrcsetclem9  18239  funcsetcestrclem9  18254  fullsetcestrc  18257  1stfcl  18288  2ndfcl  18289  hofpropd  18358  isacs3lem  18633  mgmhmlin  18804  mndpsuppss  18875  frmdss2  18975  frmdup1  18976  mgm2nsgrplem2  19034  mulgdirlem  19231  mulgass  19237  0nsg  19295  cycsubgcl  19337  ghmmulg  19358  conjghm  19379  qusghm  19385  gsumwrev  19496  symg2bas  19523  symgfixelsi  19565  f1otrspeq  19577  psgnunilem2  19625  psgnunilem3  19626  odf1o2  19703  lsmhash  19835  efgtf  19852  efginvrel2  19857  efgredeu  19882  efgcpbllemb  19885  frgpuplem  19902  frgpup1  19905  ghmcyg  20026  gsumval3lem1  20035  gsumzres  20039  gsumzcl2  20040  gsumzf1o  20042  gsumzaddlem  20051  gsumconst  20064  gsumzmhm  20067  gsumzoppg  20074  gsum2d  20102  subgdmdprd  20166  pgpfac1lem3  20209  gsummgp0  20461  rnghmmul  20593  rngcinv  20802  ringcinv  20836  islmodd  21053  lmodvsmmulgdi  21084  islss3  21146  0lmhm  21227  idlmhm  21228  lmhmeql  21242  pwssplit3  21248  cmprmidlmcl  21541  lidldvgen  21568  qsssubdrg  21642  cnsubrg  21643  znf1o  21767  psgnghm  21796  psgndif  21818  cssmre  21909  dsmmsubg  21959  frlmup1  22014  lindfrn  22037  f1lindf  22038  evlslem1  22301  psdmul  22397  coe1tmmul2  22505  pf1ind  22583  mamufval  22617  mamurid  22667  mvmulfval  22767  mdetralt2  22834  mndifsplit  22861  maducoeval2  22865  madugsum  22868  matunitlindflem1  22904  mat2pmatmul  22959  decpmatmul  23000  pm2mpf1lem  23022  pm2mpf1  23027  monmat2matmon  23052  chpscmat  23070  fvmptnn04if  23077  tgcl  23197  ppttop  23235  epttop  23237  clsval2  23278  opncldf1  23312  mretopd  23320  neindisj  23345  neiptopnei  23360  restcls  23409  restntr  23410  ordtbas  23420  cnpnei  23492  cncls2  23501  tgcmp  23629  cmpcld  23630  uncmp  23631  hauscmplem  23634  1stcfb  23673  2ndcctbss  23684  hauspwdom  23730  reftr  23743  comppfsc  23761  kgentopon  23767  ptpjpre1  23800  ptcnplem  23850  txcn  23855  txdis1cn  23864  txhaus  23876  xkopt  23884  imasnopn  23919  imasncld  23920  imasncls  23921  hmeoimaf1o  23999  cmphaushmeo  24029  txhmeo  24032  trfbas2  24072  fbasfip  24097  fbasrn  24113  fmss  24175  elfm2  24177  hauspwpwf1  24216  flfcnp  24233  fclscf  24254  flimfnfcls  24257  fcfval  24262  alexsubALTlem2  24277  alexsubALTlem3  24278  alexsubALTlem4  24279  ptcmplem3  24283  ptcmplem4  24284  cnextfval  24291  cnextcn  24296  tmdgsum2  24325  ustex2sym  24446  neipcfilu  24524  imasdsf1olem  24602  metss2lem  24740  stdbdxmet  24744  stdbdmopn  24747  metrest  24753  metcnp  24770  restmetu  24799  tngngp  24883  icccmplem1  25052  icccvx  25181  evth  25190  lebnumlem1  25192  pi1blem  25270  isncvsngp  25380  equivcau  25531  bcthlem5  25559  cmslssbn  25603  ivthlem3  25684  ovolicc2lem3  25750  ovolicc2lem4  25751  dyaddisj  25827  dyadmbllem  25830  ismbfd  25870  itg2seq  25973  itgss  26042  limciun  26124  dvcobr  26176  dvmptfsum  26205  c1liplem1  26226  c1lip1  26227  lhop  26246  dvcvx  26250  tdeglem4  26288  plyco0  26420  elply2  26424  plypf1  26441  dgreq0  26494  elqaalem2  26555  aalioulem6  26576  aaliou  26577  aaliou2b  26580  ulmss  26636  ulmcn  26638  pserulm  26661  lgamgulmlem5  27272  basellem4  27323  fsumdvdsdiaglem  27422  mpodvdsmulf1o  27433  dvdsmulf1o  27435  chtublem  27450  fsumvma2  27453  logfaclbnd  27461  dchrelbasd  27478  lgsqrlem2  27586  gausslemma2dlem1a  27604  lgseisenlem2  27615  lgsquadlem1  27619  lgsquadlem2  27620  lgsquadlem3  27621  rplogsumlem2  27724  rpvmasumlem  27726  dchrmusum2  27733  dchrvmasumlem1  27734  dchrvmasum2lem  27735  rpvmasum2  27751  dchrisum0lem1  27755  logsqvma  27781  selberg4  27800  pntibndlem3  27831  pntlem3  27848  ostthlem1  27866  ostthlem2  27867  ltsres  27901  nogt01o  27935  oldbdayim  28157  addsproplem2  28238  negsproplem2  28297  mulsval  28377  om2noseqrdg  28572  noseqrdgfn  28574  zmulscld  28665  recut  28762  idmot  28882  brcgr  29360  brbtwn2  29365  axsegconlem8  29384  axpaschlem  29400  axeuclid  29423  axcontlem2  29425  axcontlem7  29430  eengtrkg  29446  upgrex  29552  subgrprop3  29739  subupgr  29750  nbgr0edglem  29819  nb3grprlem1  29843  cusgredg  29887  cusgrres  29911  usgredgsscusgredg  29922  finsumvtxdg2ssteplem4  30011  finsumvtxdg2sstep  30012  wlkl1loop  30100  wlkp1lem4  30137  wwlksnred  30363  wwlksnext  30364  wwlksnextwrd  30368  wpthswwlks2on  30435  clwwlknp  30510  clwwlkel  30519  wwlksext2clwwlk  30530  clwwlknonwwlknonb  30579  3wlkond  30654  1conngr  30677  eucrctshift  30726  fusgr2wsp2nb  30817  numclwwlk1lem2foa  30837  numclwwlk1lem2f1  30840  numclwlk1lem1  30852  numclwlk1lem2  30853  grpoidinvlem1  30988  grporcan  31002  ipblnfi  31339  hvmulcan2  31557  shscli  31801  spansneleq  32054  pjspansn  32061  3oalem2  32147  eigposi  32320  cnlnadjlem2  32552  stlesi  32725  mdslmd1lem1  32809  mdslmd1lem2  32810  cdj1i  32917  disjxpin  33064  nn0xmulclb  33245  xreceu  33370  txomap  34347  pstmxmet  34410  qqhghm  34501  qqhrhm  34502  measinblem  34734  cntmeas  34740  ballotlemsf1o  35028  bnj945  35286  bnj1110  35494  rankfilimbi  35612  cvmopnlem  35860  cvmfolem  35861  cvmliftmolem2  35864  cvmlift2lem10  35894  satf00  35956  satffunlem2lem1  35986  satefvfmla0  36000  mrsubvrs  36104  wzel  36404  btwnconn1lem8  36677  btwnconn1lem9  36678  btwnconn1lem10  36679  btwnconn1lem11  36680  btwnconn1lem12  36681  finminlem  36940  nn0prpwlem  36944  fnessref  36979  refssfne  36980  fnemeet2  36989  consym1  37042  bj-finsumval0  38040  topdifinffinlem  38104  relowlssretop  38120  rdgeqoa  38127  fvineqsneu  38168  pibt2  38174  poimirlem28  38400  mblfinlem1  38409  mblfinlem3  38411  mblfinlem4  38412  ovoliunnfl  38414  mbfresfi  38418  mbfposadd  38419  itg2addnclem2  38424  itg2addnc  38426  ftc1anc  38453  frinfm  38488  fdc  38498  blssp  38509  sstotbnd  38528  isbnd2  38536  ssbnd  38541  prdstotbnd  38547  prdsbnd2  38548  ismtyres  38561  heibor1lem  38562  rrnequiv  38588  rngoisocnv  38734  crngohomfo  38759  pridlc3  38826  membpartlem19  39665  prter3  39758  ax12eq  39817  ax12el  39818  cvratlem  40297  islvol2aN  40468  4atlem4b  40476  4atlem4c  40477  4atlem4d  40478  isline2  40650  isline3  40652  pclfinclN  40826  linepsubclN  40827  pexmidlem4N  40849  diaglbN  41931  dvhvaddcl  41971  dvhvaddcomN  41972  dvhvscacl  41979  djavalN  42011  dibglbN  42042  dihatexv  42214  djhval  42274  mapdrvallem2  42521  evlselvlem  43437  evlselv  43438  mhpind  43443  prjsprellsp  43460  elrfi  43542  nacsfix  43560  eldioph2  43610  lzenom  43618  rexrabdioph  43638  irrapxlem3  43668  pellexlem5  43677  pellex  43679  pell1234qrne0  43697  pell1234qrmulcl  43699  pell14qrdich  43713  pell1qrge1  43714  pellqrex  43723  rmxypairf1o  43755  rmxycomplete  43761  monotoddzzfi  43786  congadd  43810  jm2.19lem3  43835  jm2.19lem4  43836  jm2.25  43843  jm2.26a  43844  jm2.26lem3  43845  expdiophlem1  43865  wepwsolem  43886  lmhmfgsplit  43930  aaitgo  44006  mon1psubm  44043  deg1mhm  44044  succlg  44172  ofoacom  44205  iunrelexp0  44545  isotone2  44892  mnuprdlem4  45102  relpmin  45778  disjrnmpt2  46023  mullimc  46449  mullimcf  46456  climxrre  46581  fprodcncf  46731  stoweidlem17  46848  stoweidlem27  46858  stoweidlem54  46885  fourierdlem42  46980  fourierdlem62  46999  fourierdlem73  47010  fourierdlem76  47013  fourierdlem97  47034  sge0iunmptlemfi  47244  isomenndlem  47361  imarnf1pr  48173  smonoord  48268  fvelsetpreimafv  48290  iccpartiltu  48325  sprsymrelf1lem  48394  prproropf1olem3  48408  paireqne  48414  fmtnoprmfac1  48471  prmdvdsfmtnof1lem2  48491  nprmdvdsfacm1  48530  gricushgr  48836  grimedg  48854  cycl3grtri  48866  gpgedg2iv  48986  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  rngcinvALTV  49194  funcringcsetcALTV2lem9  49216  ringcinvALTV  49228  funcringcsetclem9ALTV  49239  lmodvsmdi  49312  lincsum  49362  lindslinindimp2lem4  49394  nn0sumshdiglemB  49553  1arymaptf1  49575  2arymaptf1  49586  dmrnxp  49768  xpco2  49788  initopropd  50172  termopropd  50173  zeroopropd  50174  oduoppcciso  50495  lanpropd  50544  ranpropd  50545