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  4821  prproe  4872  fr2nr  5640  wereu2  5660  f1oprg  6871  fvtp1g  7202  funfvima3  7241  f1resveqaeq  7276  isof1oidb  7331  isomin  7344  weniso  7363  elovmpt3rab1  7680  sorpssi  7736  resf1extb  7937  poseq  8160  suppofssd  8205  tfrlem9a  8379  oalimcl  8551  odi  8570  oeeui  8594  ralxpmap  8900  boxriin  8944  domdifsn  9055  domunsncan  9072  enfixsn  9081  disjen  9129  mapen  9136  mapxpen  9138  mapunen  9141  findcard2d  9158  unxpdomlem2  9224  unxpdomlem3  9225  isfinite2  9265  marypha1lem  9400  marypha2  9406  supmo  9419  infmo  9464  card2inf  9524  brwdom2  9542  wemapwe  9673  rankonidlem  9807  rankxplim3  9860  djulf1o  9914  djurf1o  9915  infxpenlem  10013  infxpenc2lem1  10019  infxpenc2  10022  fseqenlem1  10024  fseqenlem2  10025  infpwfien  10062  dfac12lem2  10144  infunsdom1  10211  infunsdom  10212  infmap2  10216  fin2i2  10317  fin23lem28  10339  fin23lem32  10343  fin23lem34  10345  fin23lem40  10350  isf32lem2  10353  compssiso  10373  isfin1-3  10385  fin1a2lem10  10408  fin12  10412  hsmexlem4  10428  ac6num  10478  ttukeylem7  10514  axdclem2  10519  iundom2g  10541  fpwwe2lem11  10643  pwfseqlem3  10662  winalim2  10698  winafp  10699  wunex2  10740  grur1  10822  dedekindle  11391  00id  11402  receu  11876  lt2mul2div  12110  peano5uzi  12703  uzwo  12953  qbtwnre  13243  iooshf  13471  modmul1  13980  seqcl2  14076  seqfveq2  14080  seqid2  14104  seqdistr  14109  expcl2lem  14129  mulexpz  14158  expnlbnd2  14290  hashfun  14494  hashfacen  14511  hashf1lem1  14512  elss2prb  14545  fstwrdne0  14613  swrdsb0eq  14725  swrdswrd  14766  wrd2ind  14784  swrdccatin1  14786  pfxccatin12  14794  splid  14814  repswrevw  14850  cshwidxmod  14866  cshwidx0  14869  2cshw  14876  cshweqrep  14884  cshw1  14885  wwlktovfo  15021  relexpfld  15112  relexpindlem  15126  01sqrexlem6  15324  absexpz  15382  o1rlimmul  15696  iseralt  15762  summolem2  15792  fsumf1o  15799  fsum0diag2  15859  fsummulc2  15860  cvgcmpce  15895  incexclem  15915  prodmolem2  16014  fprodcl2lem  16029  fprodmul  16039  fprodrev  16056  moddvds  16345  dvdsflip  16399  bitsf1ocnv  16526  sadcaddlem  16539  bezoutlem2  16622  bezoutlem4  16624  dfgcd2  16628  lcmgcdlem  16688  crth  16861  hashgcdlem  16871  phisum  16874  pcqcl  16940  pcid  16957  pcneg  16958  prmpwdvds  16988  pockthg  16990  4sqlem11  17039  ramub2  17098  0ram  17104  prmgaplem7  17141  prmgaplem8  17142  setscom  17264  qusval  17620  initoeu1  18092  termoeu1  18099  setcinv  18171  funcestrcsetclem9  18228  funcsetcestrclem9  18243  fullsetcestrc  18246  1stfcl  18277  2ndfcl  18278  hofpropd  18347  isacs3lem  18622  mgmhmlin  18791  mndpsuppss  18862  frmdss2  18961  frmdup1  18962  mgm2nsgrplem2  19020  mulgdirlem  19217  mulgass  19223  0nsg  19281  cycsubgcl  19323  ghmmulg  19344  conjghm  19365  qusghm  19371  gsumwrev  19482  symg2bas  19509  symgfixelsi  19551  f1otrspeq  19563  psgnunilem2  19611  psgnunilem3  19612  odf1o2  19689  lsmhash  19821  efgtf  19838  efginvrel2  19843  efgredeu  19868  efgcpbllemb  19871  frgpuplem  19888  frgpup1  19891  ghmcyg  20012  gsumval3lem1  20021  gsumzres  20025  gsumzcl2  20026  gsumzf1o  20028  gsumzaddlem  20037  gsumconst  20050  gsumzmhm  20053  gsumzoppg  20060  gsum2d  20088  subgdmdprd  20152  pgpfac1lem3  20195  gsummgp0  20447  rnghmmul  20579  rngcinv  20788  ringcinv  20822  islmodd  21039  lmodvsmmulgdi  21070  islss3  21132  0lmhm  21213  idlmhm  21214  lmhmeql  21228  pwssplit3  21234  cmprmidlmcl  21527  lidldvgen  21554  qsssubdrg  21628  cnsubrg  21629  znf1o  21753  psgnghm  21782  psgndif  21804  cssmre  21895  dsmmsubg  21945  frlmup1  22000  lindfrn  22023  f1lindf  22024  evlslem1  22285  psdmul  22381  coe1tmmul2  22489  pf1ind  22567  mamufval  22601  mamurid  22651  mvmulfval  22751  mdetralt2  22818  mndifsplit  22845  maducoeval2  22849  madugsum  22852  mat2pmatmul  22940  decpmatmul  22981  pm2mpf1lem  23003  pm2mpf1  23008  monmat2matmon  23033  chpscmat  23051  fvmptnn04if  23058  tgcl  23178  ppttop  23216  epttop  23218  clsval2  23259  opncldf1  23293  mretopd  23301  neindisj  23326  neiptopnei  23341  restcls  23390  restntr  23391  ordtbas  23401  cnpnei  23473  cncls2  23482  tgcmp  23610  cmpcld  23611  uncmp  23612  hauscmplem  23615  1stcfb  23654  2ndcctbss  23665  hauspwdom  23711  reftr  23724  comppfsc  23742  kgentopon  23748  ptpjpre1  23781  ptcnplem  23831  txcn  23836  txdis1cn  23845  txhaus  23857  xkopt  23865  imasnopn  23900  imasncld  23901  imasncls  23902  hmeoimaf1o  23980  cmphaushmeo  24010  txhmeo  24013  trfbas2  24053  fbasfip  24078  fbasrn  24094  fmss  24156  elfm2  24158  hauspwpwf1  24197  flfcnp  24214  fclscf  24235  flimfnfcls  24238  fcfval  24243  alexsubALTlem2  24258  alexsubALTlem3  24259  alexsubALTlem4  24260  ptcmplem3  24264  ptcmplem4  24265  cnextfval  24272  cnextcn  24277  tmdgsum2  24306  ustex2sym  24427  neipcfilu  24505  imasdsf1olem  24583  metss2lem  24721  stdbdxmet  24725  stdbdmopn  24728  metrest  24734  metcnp  24751  restmetu  24780  tngngp  24864  icccmplem1  25033  icccvx  25162  evth  25171  lebnumlem1  25173  pi1blem  25251  isncvsngp  25361  equivcau  25512  bcthlem5  25540  cmslssbn  25584  ivthlem3  25665  ovolicc2lem3  25731  ovolicc2lem4  25732  dyaddisj  25808  dyadmbllem  25811  ismbfd  25851  itg2seq  25954  itgss  26024  limciun  26106  dvcobr  26158  dvmptfsum  26187  c1liplem1  26208  c1lip1  26209  lhop  26228  dvcvx  26232  tdeglem4  26270  plyco0  26402  elply2  26406  plypf1  26422  dgreq0  26475  elqaalem2  26534  aalioulem6  26553  aaliou  26554  aaliou2b  26557  ulmss  26613  ulmcn  26615  pserulm  26638  lgamgulmlem5  27250  basellem4  27301  fsumdvdsdiaglem  27400  mpodvdsmulf1o  27411  dvdsmulf1o  27413  chtublem  27428  fsumvma2  27431  logfaclbnd  27439  dchrelbasd  27456  lgsqrlem2  27564  gausslemma2dlem1a  27582  lgseisenlem2  27593  lgsquadlem1  27597  lgsquadlem2  27598  lgsquadlem3  27599  rplogsumlem2  27702  rpvmasumlem  27704  dchrmusum2  27711  dchrvmasumlem1  27712  dchrvmasum2lem  27713  rpvmasum2  27729  dchrisum0lem1  27733  logsqvma  27759  selberg4  27778  pntibndlem3  27809  pntlem3  27826  ostthlem1  27844  ostthlem2  27845  ltsres  27879  nogt01o  27913  oldbdayim  28135  addsproplem2  28216  negsproplem2  28275  mulsval  28355  om2noseqrdg  28550  noseqrdgfn  28552  zmulscld  28643  recut  28740  idmot  28859  brcgr  29307  brbtwn2  29312  axsegconlem8  29331  axpaschlem  29347  axeuclid  29370  axcontlem2  29372  axcontlem7  29377  eengtrkg  29393  upgrex  29499  subgrprop3  29686  subupgr  29697  nbgr0edglem  29766  nb3grprlem1  29790  cusgredg  29834  cusgrres  29858  usgredgsscusgredg  29869  finsumvtxdg2ssteplem4  29958  finsumvtxdg2sstep  29959  wlkl1loop  30047  wlkp1lem4  30084  wwlksnred  30310  wwlksnext  30311  wwlksnextwrd  30315  wpthswwlks2on  30382  clwwlknp  30457  clwwlkel  30466  wwlksext2clwwlk  30477  clwwlknonwwlknonb  30526  3wlkond  30595  1conngr  30618  eucrctshift  30667  fusgr2wsp2nb  30758  numclwwlk1lem2foa  30778  numclwwlk1lem2f1  30781  numclwlk1lem1  30793  numclwlk1lem2  30794  grpoidinvlem1  30929  grporcan  30943  ipblnfi  31280  hvmulcan2  31498  shscli  31742  spansneleq  31995  pjspansn  32002  3oalem2  32088  eigposi  32261  cnlnadjlem2  32493  stlesi  32666  mdslmd1lem1  32750  mdslmd1lem2  32751  cdj1i  32858  disjxpin  33006  nn0xmulclb  33188  xreceu  33313  txomap  34290  pstmxmet  34353  qqhghm  34444  qqhrhm  34445  measinblem  34677  cntmeas  34683  ballotlemsf1o  34971  bnj945  35229  bnj1110  35437  rankfilimbi  35555  cvmopnlem  35809  cvmfolem  35810  cvmliftmolem2  35813  cvmlift2lem10  35843  satf00  35905  satffunlem2lem1  35935  satefvfmla0  35949  mrsubvrs  36053  wzel  36353  btwnconn1lem8  36625  btwnconn1lem9  36626  btwnconn1lem10  36627  btwnconn1lem11  36628  btwnconn1lem12  36629  finminlem  36888  nn0prpwlem  36892  fnessref  36927  refssfne  36928  fnemeet2  36937  consym1  36990  bj-finsumval0  37988  topdifinffinlem  38052  relowlssretop  38068  rdgeqoa  38075  fvineqsneu  38116  pibt2  38122  matunitlindflem1  38326  poimirlem28  38358  mblfinlem1  38367  mblfinlem3  38369  mblfinlem4  38370  ovoliunnfl  38372  mbfresfi  38376  mbfposadd  38377  itg2addnclem2  38382  itg2addnc  38384  ftc1anc  38411  frinfm  38446  fdc  38456  blssp  38467  sstotbnd  38486  isbnd2  38494  ssbnd  38499  prdstotbnd  38505  prdsbnd2  38506  ismtyres  38519  heibor1lem  38520  rrnequiv  38546  rngoisocnv  38692  crngohomfo  38717  pridlc3  38784  membpartlem19  39623  prter3  39716  ax12eq  39775  ax12el  39776  cvratlem  40255  islvol2aN  40426  4atlem4b  40434  4atlem4c  40435  4atlem4d  40436  isline2  40608  isline3  40610  pclfinclN  40784  linepsubclN  40785  pexmidlem4N  40807  diaglbN  41889  dvhvaddcl  41929  dvhvaddcomN  41930  dvhvscacl  41937  djavalN  41969  dibglbN  42000  dihatexv  42172  djhval  42232  mapdrvallem2  42479  evlselvlem  43380  evlselv  43381  mhpind  43386  prjsprellsp  43403  elrfi  43485  nacsfix  43503  eldioph2  43553  lzenom  43561  rexrabdioph  43581  irrapxlem3  43611  pellexlem5  43620  pellex  43622  pell1234qrne0  43640  pell1234qrmulcl  43642  pell14qrdich  43656  pell1qrge1  43657  pellqrex  43666  rmxypairf1o  43698  rmxycomplete  43704  monotoddzzfi  43729  congadd  43753  jm2.19lem3  43778  jm2.19lem4  43779  jm2.25  43786  jm2.26a  43787  jm2.26lem3  43788  expdiophlem1  43808  wepwsolem  43829  lmhmfgsplit  43873  aaitgo  43949  mon1psubm  43986  deg1mhm  43987  succlg  44115  ofoacom  44148  iunrelexp0  44488  isotone2  44835  mnuprdlem4  45045  relpmin  45721  disjrnmpt2  45966  mullimc  46392  mullimcf  46399  climxrre  46524  fprodcncf  46674  stoweidlem17  46791  stoweidlem27  46801  stoweidlem54  46828  fourierdlem42  46923  fourierdlem62  46942  fourierdlem73  46953  fourierdlem76  46956  fourierdlem97  46977  sge0iunmptlemfi  47187  isomenndlem  47304  imarnf1pr  48079  smonoord  48174  fvelsetpreimafv  48196  iccpartiltu  48231  sprsymrelf1lem  48300  prproropf1olem3  48314  paireqne  48320  fmtnoprmfac1  48377  prmdvdsfmtnof1lem2  48397  nprmdvdsfacm1  48436  gricushgr  48742  grimedg  48760  cycl3grtri  48772  gpgedg2iv  48892  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  rngcinvALTV  49100  funcringcsetcALTV2lem9  49122  ringcinvALTV  49134  funcringcsetclem9ALTV  49145  lmodvsmdi  49218  lincsum  49268  lindslinindimp2lem4  49300  nn0sumshdiglemB  49459  1arymaptf1  49481  2arymaptf1  49492  dmrnxp  49674  xpco2  49694  initopropd  50080  termopropd  50081  zeroopropd  50082  oduoppcciso  50403  lanpropd  50452  ranpropd  50453