Theorem ad2antll 726

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

This theorem is referenced by:  simprr  770  simprrl  778  simprrr  779  simprr1  1220  simprr2  1221  simprr3  1222  prneimg  4786  fr2nr  5568  wereu2  5587  f1oprg  6770  fvtp1g  7082  funfvima3  7121  isof1oidb  7204  isomin  7217  weniso  7234  elovmpt3rab1  7538  sorpssi  7591  suppofssd  8028  tfrlem9a  8226  oalimcl  8400  odi  8419  oeeui  8442  ralxpmap  8693  boxriin  8737  domdifsn  8850  domunsncan  8868  enfixsn  8877  disjen  8930  mapen  8937  mapxpen  8939  mapunen  8942  findcard2d  8958  unxpdomlem2  9037  unxpdomlem3  9038  findcard3  9066  isfinite2  9081  marypha1lem  9201  marypha2  9207  supmo  9220  infmo  9263  card2inf  9323  brwdom2  9341  wemapwe  9464  rankonidlem  9595  rankxplim3  9648  djulf1o  9679  djurf1o  9680  infxpenlem  9778  infxpenc2lem1  9784  infxpenc2  9787  fseqenlem1  9789  fseqenlem2  9790  infpwfien  9827  dfac12lem2  9909  infunsdom1  9978  infunsdom  9979  infmap2  9983  fin2i2  10083  fin23lem28  10105  fin23lem32  10109  fin23lem34  10111  fin23lem40  10116  isf32lem2  10119  compssiso  10139  isfin1-3  10151  fin1a2lem10  10174  fin12  10178  hsmexlem4  10194  ac6num  10244  ttukeylem7  10280  axdclem2  10285  iundom2g  10305  fpwwe2lem11  10406  pwfseqlem3  10425  winalim2  10461  winafp  10462  wunex2  10503  grur1  10585  dedekindle  11148  00id  11159  receu  11629  lt2mul2div  11862  peano5uzi  12418  uzwo  12660  qbtwnre  12942  iooshf  13167  modmul1  13653  seqcl2  13750  seqfveq2  13754  seqid2  13778  seqdistr  13783  expcl2lem  13803  mulexpz  13832  expnlbnd2  13958  hashfun  14161  hashfacen  14175  hashfacenOLD  14176  hashf1lem1  14177  hashf1lem1OLD  14178  elss2prb  14210  fstwrdne0  14268  swrdsb0eq  14385  swrdswrd  14427  wrd2ind  14445  swrdccatin1  14447  pfxccatin12  14455  splid  14475  repswrevw  14509  cshwidxmod  14525  cshwidx0  14528  2cshw  14535  cshweqrep  14543  cshw1  14544  wwlktovfo  14682  relexpfld  14769  relexpindlem  14783  sqrlem6  14968  absexpz  15026  o1rlimmul  15337  iseralt  15405  summolem2  15437  fsumf1o  15444  fsum0diag2  15504  fsummulc2  15505  cvgcmpce  15539  incexclem  15557  prodmolem2  15654  fprodcl2lem  15669  fprodmul  15679  fprodrev  15696  moddvds  15983  dvdsflip  16035  bitsf1ocnv  16160  sadcaddlem  16173  bezoutlem2  16257  bezoutlem4  16259  dfgcd2  16263  lcmgcdlem  16320  crth  16488  hashgcdlem  16498  phisum  16500  pcqcl  16566  pcid  16583  pcneg  16584  prmpwdvds  16614  pockthg  16616  4sqlem11  16665  ramub2  16724  0ram  16730  prmgaplem7  16767  prmgaplem8  16768  setscom  16890  qusval  17262  initoeu1  17735  termoeu1  17742  setcinv  17814  funcestrcsetclem9  17874  funcsetcestrclem9  17889  fullsetcestrc  17892  1stfcl  17923  2ndfcl  17924  hofpropd  17994  isacs3lem  18269  frmdss2  18511  frmdup1  18512  mgm2nsgrplem2  18567  mulgdirlem  18743  mulgass  18749  0nsg  18806  cycsubgcl  18834  ghmmulg  18855  conjghm  18874  qusghm  18880  gsumwrev  18982  symg2bas  19009  symgfixelsi  19052  f1otrspeq  19064  psgnunilem2  19112  psgnunilem3  19113  odf1o2  19187  lsmhash  19320  efgtf  19337  efginvrel2  19342  efgredeu  19367  efgcpbllemb  19370  frgpuplem  19387  frgpup1  19390  cygablOLD  19501  ghmcyg  19506  gsumval3lem1  19515  gsumzres  19519  gsumzcl2  19520  gsumzf1o  19522  gsumzaddlem  19531  gsumconst  19544  gsumzmhm  19547  gsumzoppg  19554  gsum2d  19582  subgdmdprd  19646  pgpfac1lem3  19689  gsummgp0  19856  islmodd  20138  lmodvsmmulgdi  20167  islss3  20230  0lmhm  20311  idlmhm  20312  lmhmeql  20326  pwssplit3  20332  lidldvgen  20535  qsssubdrg  20666  cnsubrg  20667  znf1o  20768  psgnghm  20794  psgndif  20816  cssmre  20907  dsmmsubg  20959  frlmup1  21014  lindfrn  21037  f1lindf  21038  evlslem1  21301  coe1tmmul2  21456  pf1ind  21530  mamufval  21543  mamurid  21600  mvmulfval  21700  mdetralt2  21767  mndifsplit  21794  maducoeval2  21798  madugsum  21801  mat2pmatmul  21889  decpmatmul  21930  pm2mpf1lem  21952  pm2mpf1  21957  monmat2matmon  21982  chpscmat  22000  fvmptnn04if  22007  tgcl  22128  ppttop  22166  epttop  22168  clsval2  22210  opncldf1  22244  mretopd  22252  neindisj  22277  neiptopnei  22292  restcls  22341  restntr  22342  ordtbas  22352  cnpnei  22424  cncls2  22433  tgcmp  22561  cmpcld  22562  uncmp  22563  hauscmplem  22566  1stcfb  22605  2ndcctbss  22615  hauspwdom  22661  reftr  22674  comppfsc  22692  kgentopon  22698  ptpjpre1  22731  ptcnplem  22781  txcn  22786  txdis1cn  22795  txhaus  22807  xkopt  22815  imasnopn  22850  imasncld  22851  imasncls  22852  hmeoimaf1o  22930  cmphaushmeo  22960  txhmeo  22963  trfbas2  23003  fbasfip  23028  fbasrn  23044  fmss  23106  elfm2  23108  hauspwpwf1  23147  flfcnp  23164  fclscf  23185  flimfnfcls  23188  fcfval  23193  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  ptcmplem3  23214  ptcmplem4  23215  cnextfval  23222  cnextcn  23227  tmdgsum2  23256  ustex2sym  23377  neipcfilu  23457  imasdsf1olem  23535  metss2lem  23676  stdbdxmet  23680  stdbdmopn  23683  metrest  23689  metcnp  23706  restmetu  23735  tngngp  23827  icccmplem1  23994  icccvx  24122  evth  24131  lebnumlem1  24133  pi1blem  24211  isncvsngp  24322  equivcau  24473  bcthlem5  24501  cmslssbn  24545  ivthlem3  24626  ovolicc2lem3  24692  ovolicc2lem4  24693  dyaddisj  24769  dyadmbllem  24772  ismbfd  24812  itg2seq  24916  itgss  24985  limciun  25067  dvcobr  25119  dvmptfsum  25148  c1liplem1  25169  c1lip1  25170  lhop  25189  dvcvx  25193  tdeglem4  25233  plyco0  25362  elply2  25366  plypf1  25382  dgreq0  25435  elqaalem2  25489  aalioulem6  25506  aaliou  25507  aaliou2b  25510  ulmss  25565  ulmcn  25567  pserulm  25590  lgamgulmlem5  26191  basellem4  26242  fsumdvdsdiaglem  26341  dvdsmulf1o  26352  chtublem  26368  fsumvma2  26371  logfaclbnd  26379  dchrelbasd  26396  lgsqrlem2  26504  gausslemma2dlem1a  26522  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  rplogsumlem2  26642  rpvmasumlem  26644  dchrmusum2  26651  dchrvmasumlem1  26652  dchrvmasum2lem  26653  rpvmasum2  26669  dchrisum0lem1  26673  logsqvma  26699  selberg4  26718  pntibndlem3  26749  pntlem3  26766  ostthlem1  26784  ostthlem2  26785  idmot  26907  brcgr  27277  brbtwn2  27282  axsegconlem8  27301  axpaschlem  27317  axeuclid  27340  axcontlem2  27342  axcontlem7  27347  eengtrkg  27363  upgrex  27471  subgrprop3  27652  subupgr  27663  nbgr0vtxlem  27731  nb3grprlem1  27756  cusgredg  27800  cusgrres  27824  usgredgsscusgredg  27835  finsumvtxdg2ssteplem4  27924  finsumvtxdg2sstep  27925  wlkl1loop  28014  wlkp1lem4  28053  wwlksnred  28266  wwlksnext  28267  wwlksnextwrd  28271  wpthswwlks2on  28335  clwwlknp  28410  clwwlkel  28419  wwlksext2clwwlk  28430  clwwlknonwwlknonb  28479  3wlkond  28544  1conngr  28567  eucrctshift  28616  fusgr2wsp2nb  28707  numclwwlk1lem2foa  28727  numclwwlk1lem2f1  28730  numclwlk1lem1  28742  numclwlk1lem2  28743  grpoidinvlem1  28875  grporcan  28889  ipblnfi  29226  hvmulcan2  29444  shscli  29688  spansneleq  29941  pjspansn  29948  3oalem2  30034  eigposi  30207  cnlnadjlem2  30439  stlesi  30612  mdslmd1lem1  30696  mdslmd1lem2  30697  cdj1i  30804  disjxpin  30936  nn0xmulclb  31103  xreceu  31205  txomap  31793  pstmxmet  31856  qqhghm  31947  qqhrhm  31948  measinblem  32197  cntmeas  32203  ballotlemsf1o  32489  bnj945  32762  bnj1110  32971  f1resveqaeq  33066  cvmopnlem  33249  cvmfolem  33250  cvmliftmolem2  33253  cvmlift2lem10  33283  satf00  33345  satffunlem2lem1  33375  satefvfmla0  33389  mrsubvrs  33493  poxp3  33805  poseq  33811  wzel  33827  sltres  33874  nogt01o  33908  oldbdayim  34080  btwnconn1lem8  34405  btwnconn1lem9  34406  btwnconn1lem10  34407  btwnconn1lem11  34408  btwnconn1lem12  34409  finminlem  34516  nn0prpwlem  34520  fnessref  34555  refssfne  34556  fnemeet2  34565  consym1  34618  bj-finsumval0  35465  topdifinffinlem  35527  relowlssretop  35543  rdgeqoa  35550  fvineqsneu  35591  pibt2  35597  matunitlindflem1  35782  poimirlem28  35814  mblfinlem1  35823  mblfinlem3  35825  mblfinlem4  35826  ovoliunnfl  35828  mbfresfi  35832  mbfposadd  35833  itg2addnclem2  35838  itg2addnc  35840  ftc1anc  35867  frinfm  35902  fdc  35912  blssp  35923  sstotbnd  35942  isbnd2  35950  ssbnd  35955  prdstotbnd  35961  prdsbnd2  35962  ismtyres  35975  heibor1lem  35976  rrnequiv  36002  rngoisocnv  36148  crngohomfo  36173  pridlc3  36240  prter3  36903  ax12eq  36962  ax12el  36963  cvratlem  37442  islvol2aN  37613  4atlem4b  37621  4atlem4c  37622  4atlem4d  37623  isline2  37795  isline3  37797  pclfinclN  37971  linepsubclN  37972  pexmidlem4N  37994  diaglbN  39076  dvhvaddcl  39116  dvhvaddcomN  39117  dvhvscacl  39124  djavalN  39156  dibglbN  39187  dihatexv  39359  djhval  39419  mapdrvallem2  39666  metakunt15  40146  mhpind  40290  prjsprellsp  40457  elrfi  40523  nacsfix  40541  eldioph2  40591  lzenom  40599  rexrabdioph  40623  irrapxlem3  40653  pellexlem5  40662  pellex  40664  pell1234qrne0  40682  pell1234qrmulcl  40684  pell14qrdich  40698  pell1qrge1  40699  pellqrex  40708  rmxypairf1o  40740  rmxycomplete  40746  monotoddzzfi  40771  congadd  40795  jm2.19lem3  40820  jm2.19lem4  40821  jm2.25  40828  jm2.26a  40829  jm2.26lem3  40830  expdiophlem1  40850  wepwsolem  40874  lmhmfgsplit  40918  aaitgo  40994  mon1psubm  41038  deg1mhm  41039  iunrelexp0  41317  isotone2  41666  mnuprdlem4  41900  disjrnmpt2  42733  mullimc  43164  mullimcf  43171  climxrre  43298  fprodcncf  43448  stoweidlem17  43565  stoweidlem27  43575  stoweidlem54  43602  fourierdlem42  43697  fourierdlem62  43716  fourierdlem73  43727  fourierdlem76  43730  fourierdlem97  43751  sge0iunmptlemfi  43958  isomenndlem  44075  ovnsslelem  44105  imarnf1pr  44785  smonoord  44834  fvelsetpreimafv  44850  iccpartiltu  44885  sprsymrelf1lem  44954  prproropf1olem3  44968  paireqne  44974  fmtnoprmfac1  45028  prmdvdsfmtnof1lem2  45048  isomushgr  45289  isomuspgrlem2c  45293  mgmhmlin  45351  rnghmmul  45469  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  funcringcsetcALTV2lem9  45613  ringcinvALTV  45625  funcringcsetclem9ALTV  45636  mndpsuppss  45718  lmodvsmdi  45729  lincsum  45781  lindslinindimp2lem4  45813  nn0sumshdiglemB  45977  1arymaptf1  45999  2arymaptf1  46010