Theorem ad2antll 735

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 482	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜓)
3	2	adantl 482	1 ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  simprr  778  simprrl  786  simprrr  787  simprr1  1228  simprr2  1229  simprr3  1230  prneimg  4786  prproe  4837  fr2nr  5596  wereu2  5616  f1oprg  6814  fvtp1g  7143  funfvima3  7181  isof1oidb  7269  isomin  7282  weniso  7299  elovmpt3rab1  7617  sorpssi  7673  resf1extb  7875  poseq  8099  suppofssd  8144  tfrlem9a  8316  oalimcl  8486  odi  8505  oeeui  8529  ralxpmap  8835  boxriin  8879  domdifsn  8989  domunsncan  9006  enfixsn  9015  disjen  9063  mapen  9070  mapxpen  9072  mapunen  9075  findcard2d  9092  unxpdomlem2  9158  unxpdomlem3  9159  isfinite2  9199  marypha1lem  9337  marypha2  9343  supmo  9356  infmo  9401  card2inf  9461  brwdom2  9479  wemapwe  9610  rankonidlem  9744  rankxplim3  9797  djulf1o  9828  djurf1o  9829  infxpenlem  9927  infxpenc2lem1  9933  infxpenc2  9936  fseqenlem1  9938  fseqenlem2  9939  infpwfien  9976  dfac12lem2  10059  infunsdom1  10126  infunsdom  10127  infmap2  10131  fin2i2  10232  fin23lem28  10254  fin23lem32  10258  fin23lem34  10260  fin23lem40  10265  isf32lem2  10268  compssiso  10288  isfin1-3  10300  fin1a2lem10  10323  fin12  10327  hsmexlem4  10343  ac6num  10393  ttukeylem7  10429  axdclem2  10434  iundom2g  10454  fpwwe2lem11  10556  pwfseqlem3  10575  winalim2  10611  winafp  10612  wunex2  10653  grur1  10735  dedekindle  11302  00id  11313  receu  11787  lt2mul2div  12026  peano5uzi  12610  uzwo  12853  qbtwnre  13143  iooshf  13371  modmul1  13878  seqcl2  13974  seqfveq2  13978  seqid2  14002  seqdistr  14007  expcl2lem  14027  mulexpz  14056  expnlbnd2  14188  hashfun  14391  hashfacen  14408  hashf1lem1  14409  elss2prb  14442  fstwrdne0  14510  swrdsb0eq  14618  swrdswrd  14659  wrd2ind  14677  swrdccatin1  14679  pfxccatin12  14687  splid  14707  repswrevw  14741  cshwidxmod  14757  cshwidx0  14760  2cshw  14767  cshweqrep  14775  cshw1  14776  wwlktovfo  14912  relexpfld  15003  relexpindlem  15017  01sqrexlem6  15201  absexpz  15259  o1rlimmul  15573  iseralt  15639  summolem2  15670  fsumf1o  15677  fsum0diag2  15737  fsummulc2  15738  cvgcmpce  15773  incexclem  15793  prodmolem2  15892  fprodcl2lem  15907  fprodmul  15917  fprodrev  15934  moddvds  16224  dvdsflip  16278  bitsf1ocnv  16405  sadcaddlem  16418  bezoutlem2  16501  bezoutlem4  16503  dfgcd2  16507  lcmgcdlem  16567  crth  16740  hashgcdlem  16750  phisum  16753  pcqcl  16819  pcid  16836  pcneg  16837  prmpwdvds  16867  pockthg  16869  4sqlem11  16918  ramub2  16977  0ram  16983  prmgaplem7  17020  prmgaplem8  17021  setscom  17142  qusval  17498  initoeu1  17970  termoeu1  17977  setcinv  18049  funcestrcsetclem9  18106  funcsetcestrclem9  18121  fullsetcestrc  18124  1stfcl  18155  2ndfcl  18156  hofpropd  18225  isacs3lem  18500  mgmhmlin  18659  mndpsuppss  18725  frmdss2  18823  frmdup1  18824  mgm2nsgrplem2  18882  mulgdirlem  19073  mulgass  19079  0nsg  19136  cycsubgcl  19173  ghmmulg  19195  conjghm  19216  qusghm  19222  gsumwrev  19333  symg2bas  19360  symgfixelsi  19402  f1otrspeq  19414  psgnunilem2  19462  psgnunilem3  19463  odf1o2  19540  lsmhash  19672  efgtf  19689  efginvrel2  19694  efgredeu  19719  efgcpbllemb  19722  frgpuplem  19739  frgpup1  19742  ghmcyg  19863  gsumval3lem1  19872  gsumzres  19876  gsumzcl2  19877  gsumzf1o  19879  gsumzaddlem  19888  gsumconst  19901  gsumzmhm  19904  gsumzoppg  19911  gsum2d  19939  subgdmdprd  20003  pgpfac1lem3  20046  gsummgp0  20289  rnghmmul  20421  rngcinv  20610  ringcinv  20644  islmodd  20857  lmodvsmmulgdi  20888  islss3  20950  0lmhm  21031  idlmhm  21032  lmhmeql  21046  pwssplit3  21052  lidldvgen  21328  qsssubdrg  21402  cnsubrg  21403  znf1o  21527  psgnghm  21556  psgndif  21578  cssmre  21669  dsmmsubg  21719  frlmup1  21774  lindfrn  21797  f1lindf  21798  evlslem1  22059  psdmul  22155  coe1tmmul2  22263  pf1ind  22342  mamufval  22376  mamurid  22426  mvmulfval  22526  mdetralt2  22593  mndifsplit  22620  maducoeval2  22624  madugsum  22627  mat2pmatmul  22715  decpmatmul  22756  pm2mpf1lem  22778  pm2mpf1  22783  monmat2matmon  22808  chpscmat  22826  fvmptnn04if  22833  tgcl  22953  ppttop  22991  epttop  22993  clsval2  23034  opncldf1  23068  mretopd  23076  neindisj  23101  neiptopnei  23116  restcls  23165  restntr  23166  ordtbas  23176  cnpnei  23248  cncls2  23257  tgcmp  23385  cmpcld  23386  uncmp  23387  hauscmplem  23390  1stcfb  23429  2ndcctbss  23439  hauspwdom  23485  reftr  23498  comppfsc  23516  kgentopon  23522  ptpjpre1  23555  ptcnplem  23605  txcn  23610  txdis1cn  23619  txhaus  23631  xkopt  23639  imasnopn  23674  imasncld  23675  imasncls  23676  hmeoimaf1o  23754  cmphaushmeo  23784  txhmeo  23787  trfbas2  23827  fbasfip  23852  fbasrn  23868  fmss  23930  elfm2  23932  hauspwpwf1  23971  flfcnp  23988  fclscf  24009  flimfnfcls  24012  fcfval  24017  alexsubALTlem2  24032  alexsubALTlem3  24033  alexsubALTlem4  24034  ptcmplem3  24038  ptcmplem4  24039  cnextfval  24046  cnextcn  24051  tmdgsum2  24080  ustex2sym  24201  neipcfilu  24279  imasdsf1olem  24357  metss2lem  24495  stdbdxmet  24499  stdbdmopn  24502  metrest  24508  metcnp  24525  restmetu  24554  tngngp  24638  icccmplem1  24807  icccvx  24936  evth  24945  lebnumlem1  24947  pi1blem  25025  isncvsngp  25135  equivcau  25286  bcthlem5  25314  cmslssbn  25358  ivthlem3  25439  ovolicc2lem3  25505  ovolicc2lem4  25506  dyaddisj  25582  dyadmbllem  25585  ismbfd  25625  itg2seq  25728  itgss  25798  limciun  25880  dvcobr  25932  dvmptfsum  25961  c1liplem1  25982  c1lip1  25983  lhop  26002  dvcvx  26006  tdeglem4  26044  plyco0  26176  elply2  26180  plypf1  26196  dgreq0  26249  elqaalem2  26305  aalioulem6  26322  aaliou  26323  aaliou2b  26326  ulmss  26381  ulmcn  26383  pserulm  26406  lgamgulmlem5  27015  basellem4  27066  fsumdvdsdiaglem  27165  mpodvdsmulf1o  27176  dvdsmulf1o  27178  chtublem  27193  fsumvma2  27196  logfaclbnd  27204  dchrelbasd  27221  lgsqrlem2  27329  gausslemma2dlem1a  27347  lgseisenlem2  27358  lgsquadlem1  27362  lgsquadlem2  27363  lgsquadlem3  27364  rplogsumlem2  27467  rpvmasumlem  27469  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2lem  27478  rpvmasum2  27494  dchrisum0lem1  27498  logsqvma  27524  selberg4  27543  pntibndlem3  27574  pntlem3  27591  ostthlem1  27609  ostthlem2  27610  ltsres  27645  nogt01o  27679  oldbdayim  27900  addsproplem2  27981  negsproplem2  28040  mulsval  28120  om2noseqrdg  28315  noseqrdgfn  28317  zmulscld  28408  recut  28505  idmot  28624  brcgr  28988  brbtwn2  28993  axsegconlem8  29012  axpaschlem  29028  axeuclid  29051  axcontlem2  29053  axcontlem7  29058  eengtrkg  29074  upgrex  29180  subgrprop3  29364  subupgr  29375  nbgr0edglem  29444  nb3grprlem1  29468  cusgredg  29512  cusgrres  29536  usgredgsscusgredg  29547  finsumvtxdg2ssteplem4  29636  finsumvtxdg2sstep  29637  wlkl1loop  29725  wlkp1lem4  29762  wwlksnred  29979  wwlksnext  29980  wwlksnextwrd  29984  wpthswwlks2on  30051  clwwlknp  30126  clwwlkel  30135  wwlksext2clwwlk  30146  clwwlknonwwlknonb  30195  3wlkond  30260  1conngr  30283  eucrctshift  30332  fusgr2wsp2nb  30423  numclwwlk1lem2foa  30443  numclwwlk1lem2f1  30446  numclwlk1lem1  30458  numclwlk1lem2  30459  grpoidinvlem1  30594  grporcan  30608  ipblnfi  30945  hvmulcan2  31163  shscli  31407  spansneleq  31660  pjspansn  31667  3oalem2  31753  eigposi  31926  cnlnadjlem2  32158  stlesi  32331  mdslmd1lem1  32415  mdslmd1lem2  32416  cdj1i  32523  disjxpin  32678  nn0xmulclb  32864  xreceu  33001  txomap  34027  pstmxmet  34090  qqhghm  34181  qqhrhm  34182  measinblem  34413  cntmeas  34419  ballotlemsf1o  34707  bnj945  34965  bnj1110  35173  f1resveqaeq  35275  rankfilimbi  35291  cvmopnlem  35515  cvmfolem  35516  cvmliftmolem2  35519  cvmlift2lem10  35549  satf00  35611  satffunlem2lem1  35641  satefvfmla0  35655  mrsubvrs  35759  wzel  36059  btwnconn1lem8  36331  btwnconn1lem9  36332  btwnconn1lem10  36333  btwnconn1lem11  36334  btwnconn1lem12  36335  finminlem  36555  nn0prpwlem  36559  fnessref  36594  refssfne  36595  fnemeet2  36604  consym1  36657  bj-finsumval0  37654  topdifinffinlem  37718  relowlssretop  37734  rdgeqoa  37741  fvineqsneu  37782  pibt2  37788  matunitlindflem1  37992  poimirlem28  38024  mblfinlem1  38033  mblfinlem3  38035  mblfinlem4  38036  ovoliunnfl  38038  mbfresfi  38042  mbfposadd  38043  itg2addnclem2  38048  itg2addnc  38050  ftc1anc  38077  frinfm  38111  fdc  38121  blssp  38132  sstotbnd  38151  isbnd2  38159  ssbnd  38164  prdstotbnd  38170  prdsbnd2  38171  ismtyres  38184  heibor1lem  38185  rrnequiv  38211  rngoisocnv  38357  crngohomfo  38382  pridlc3  38449  membpartlem19  39290  prter3  39383  ax12eq  39442  ax12el  39443  cvratlem  39922  islvol2aN  40093  4atlem4b  40101  4atlem4c  40102  4atlem4d  40103  isline2  40275  isline3  40277  pclfinclN  40451  linepsubclN  40452  pexmidlem4N  40474  diaglbN  41556  dvhvaddcl  41596  dvhvaddcomN  41597  dvhvscacl  41604  djavalN  41636  dibglbN  41667  dihatexv  41839  djhval  41899  mapdrvallem2  42146  evlselvlem  43047  evlselv  43048  mhpind  43053  prjsprellsp  43070  elrfi  43152  nacsfix  43170  eldioph2  43220  lzenom  43228  rexrabdioph  43248  irrapxlem3  43278  pellexlem5  43287  pellex  43289  pell1234qrne0  43307  pell1234qrmulcl  43309  pell14qrdich  43323  pell1qrge1  43324  pellqrex  43333  rmxypairf1o  43365  rmxycomplete  43371  monotoddzzfi  43396  congadd  43420  jm2.19lem3  43445  jm2.19lem4  43446  jm2.25  43453  jm2.26a  43454  jm2.26lem3  43455  expdiophlem1  43475  wepwsolem  43496  lmhmfgsplit  43540  aaitgo  43616  mon1psubm  43653  deg1mhm  43654  succlg  43782  ofoacom  43815  iunrelexp0  44155  isotone2  44502  mnuprdlem4  44728  relpmin  45405  disjrnmpt2  45643  mullimc  46069  mullimcf  46076  climxrre  46201  fprodcncf  46351  stoweidlem17  46468  stoweidlem27  46478  stoweidlem54  46505  fourierdlem42  46600  fourierdlem62  46619  fourierdlem73  46630  fourierdlem76  46633  fourierdlem97  46654  sge0iunmptlemfi  46864  isomenndlem  46981  imarnf1pr  47753  smonoord  47848  fvelsetpreimafv  47870  iccpartiltu  47905  sprsymrelf1lem  47974  prproropf1olem3  47988  paireqne  47994  fmtnoprmfac1  48051  prmdvdsfmtnof1lem2  48071  nprmdvdsfacm1  48110  gricushgr  48416  grimedg  48434  cycl3grtri  48446  gpgedg2iv  48566  pgnbgreunbgrlem2lem1  48613  pgnbgreunbgrlem2lem2  48614  rngcinvALTV  48775  funcringcsetcALTV2lem9  48797  ringcinvALTV  48809  funcringcsetclem9ALTV  48820  lmodvsmdi  48878  lincsum  48928  lindslinindimp2lem4  48960  nn0sumshdiglemB  49119  1arymaptf1  49141  2arymaptf1  49152  dmrnxp  49335  xpco2  49355  initopropd  49741  termopropd  49742  zeroopropd  49743  oduoppcciso  50064  lanpropd  50113  ranpropd  50114