Theorem ad2antll 739

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  simprr  782  simprrl  790  simprrr  791  simprr1  1236  simprr2  1237  simprr3  1238  prneimg  4813  prproe  4864  fr2nr  5625  wereu2  5645  f1oprg  6854  fvtp1g  7183  funfvima3  7221  isof1oidb  7309  isomin  7322  weniso  7339  elovmpt3rab1  7657  sorpssi  7713  resf1extb  7916  poseq  8139  suppofssd  8184  tfrlem9a  8358  oalimcl  8530  odi  8549  oeeui  8573  ralxpmap  8879  boxriin  8923  domdifsn  9033  domunsncan  9050  enfixsn  9059  disjen  9107  mapen  9114  mapxpen  9116  mapunen  9119  findcard2d  9136  unxpdomlem2  9202  unxpdomlem3  9203  isfinite2  9243  marypha1lem  9380  marypha2  9386  supmo  9399  infmo  9444  card2inf  9504  brwdom2  9522  wemapwe  9653  rankonidlem  9787  rankxplim3  9840  djulf1o  9871  djurf1o  9872  infxpenlem  9970  infxpenc2lem1  9976  infxpenc2  9979  fseqenlem1  9981  fseqenlem2  9982  infpwfien  10019  dfac12lem2  10102  infunsdom1  10169  infunsdom  10170  infmap2  10174  fin2i2  10276  fin23lem28  10298  fin23lem32  10302  fin23lem34  10304  fin23lem40  10309  isf32lem2  10312  compssiso  10332  isfin1-3  10344  fin1a2lem10  10367  fin12  10371  hsmexlem4  10387  ac6num  10437  ttukeylem7  10473  axdclem2  10478  iundom2g  10498  fpwwe2lem11  10600  pwfseqlem3  10619  winalim2  10655  winafp  10656  wunex2  10697  grur1  10779  dedekindle  11348  00id  11359  receu  11833  lt2mul2div  12071  peano5uzi  12663  uzwo  12913  qbtwnre  13203  iooshf  13431  modmul1  13938  seqcl2  14034  seqfveq2  14038  seqid2  14062  seqdistr  14067  expcl2lem  14087  mulexpz  14116  expnlbnd2  14248  hashfun  14451  hashfacen  14468  hashf1lem1  14469  elss2prb  14502  fstwrdne0  14570  swrdsb0eq  14678  swrdswrd  14719  wrd2ind  14737  swrdccatin1  14739  pfxccatin12  14747  splid  14767  repswrevw  14801  cshwidxmod  14817  cshwidx0  14820  2cshw  14827  cshweqrep  14835  cshw1  14836  wwlktovfo  14972  relexpfld  15063  relexpindlem  15077  01sqrexlem6  15275  absexpz  15333  o1rlimmul  15647  iseralt  15713  summolem2  15744  fsumf1o  15751  fsum0diag2  15811  fsummulc2  15812  cvgcmpce  15847  incexclem  15867  prodmolem2  15966  fprodcl2lem  15981  fprodmul  15991  fprodrev  16008  moddvds  16298  dvdsflip  16352  bitsf1ocnv  16479  sadcaddlem  16492  bezoutlem2  16575  bezoutlem4  16577  dfgcd2  16581  lcmgcdlem  16641  crth  16814  hashgcdlem  16824  phisum  16827  pcqcl  16893  pcid  16910  pcneg  16911  prmpwdvds  16941  pockthg  16943  4sqlem11  16992  ramub2  17051  0ram  17057  prmgaplem7  17094  prmgaplem8  17095  setscom  17217  qusval  17573  initoeu1  18045  termoeu1  18052  setcinv  18124  funcestrcsetclem9  18181  funcsetcestrclem9  18196  fullsetcestrc  18199  1stfcl  18230  2ndfcl  18231  hofpropd  18300  isacs3lem  18575  mgmhmlin  18734  mndpsuppss  18800  frmdss2  18898  frmdup1  18899  mgm2nsgrplem2  18957  mulgdirlem  19148  mulgass  19154  0nsg  19211  cycsubgcl  19248  ghmmulg  19269  conjghm  19290  qusghm  19296  gsumwrev  19407  symg2bas  19434  symgfixelsi  19476  f1otrspeq  19488  psgnunilem2  19536  psgnunilem3  19537  odf1o2  19614  lsmhash  19746  efgtf  19763  efginvrel2  19768  efgredeu  19793  efgcpbllemb  19796  frgpuplem  19813  frgpup1  19816  ghmcyg  19937  gsumval3lem1  19946  gsumzres  19950  gsumzcl2  19951  gsumzf1o  19953  gsumzaddlem  19962  gsumconst  19975  gsumzmhm  19978  gsumzoppg  19985  gsum2d  20013  subgdmdprd  20077  pgpfac1lem3  20120  gsummgp0  20367  rnghmmul  20499  rngcinv  20688  ringcinv  20722  islmodd  20934  lmodvsmmulgdi  20965  islss3  21027  0lmhm  21108  idlmhm  21109  lmhmeql  21123  pwssplit3  21129  lidldvgen  21405  qsssubdrg  21479  cnsubrg  21480  znf1o  21604  psgnghm  21633  psgndif  21655  cssmre  21746  dsmmsubg  21796  frlmup1  21851  lindfrn  21874  f1lindf  21875  evlslem1  22136  psdmul  22232  coe1tmmul2  22340  pf1ind  22419  mamufval  22453  mamurid  22503  mvmulfval  22603  mdetralt2  22670  mndifsplit  22697  maducoeval2  22701  madugsum  22704  mat2pmatmul  22792  decpmatmul  22833  pm2mpf1lem  22855  pm2mpf1  22860  monmat2matmon  22885  chpscmat  22903  fvmptnn04if  22910  tgcl  23030  ppttop  23068  epttop  23070  clsval2  23111  opncldf1  23145  mretopd  23153  neindisj  23178  neiptopnei  23193  restcls  23242  restntr  23243  ordtbas  23253  cnpnei  23325  cncls2  23334  tgcmp  23462  cmpcld  23463  uncmp  23464  hauscmplem  23467  1stcfb  23506  2ndcctbss  23516  hauspwdom  23562  reftr  23575  comppfsc  23593  kgentopon  23599  ptpjpre1  23632  ptcnplem  23682  txcn  23687  txdis1cn  23696  txhaus  23708  xkopt  23716  imasnopn  23751  imasncld  23752  imasncls  23753  hmeoimaf1o  23831  cmphaushmeo  23861  txhmeo  23864  trfbas2  23904  fbasfip  23929  fbasrn  23945  fmss  24007  elfm2  24009  hauspwpwf1  24048  flfcnp  24065  fclscf  24086  flimfnfcls  24089  fcfval  24094  alexsubALTlem2  24109  alexsubALTlem3  24110  alexsubALTlem4  24111  ptcmplem3  24115  ptcmplem4  24116  cnextfval  24123  cnextcn  24128  tmdgsum2  24157  ustex2sym  24278  neipcfilu  24356  imasdsf1olem  24434  metss2lem  24572  stdbdxmet  24576  stdbdmopn  24579  metrest  24585  metcnp  24602  restmetu  24631  tngngp  24715  icccmplem1  24884  icccvx  25013  evth  25022  lebnumlem1  25024  pi1blem  25102  isncvsngp  25212  equivcau  25363  bcthlem5  25391  cmslssbn  25435  ivthlem3  25516  ovolicc2lem3  25582  ovolicc2lem4  25583  dyaddisj  25659  dyadmbllem  25662  ismbfd  25702  itg2seq  25805  itgss  25875  limciun  25957  dvcobr  26009  dvmptfsum  26038  c1liplem1  26059  c1lip1  26060  lhop  26079  dvcvx  26083  tdeglem4  26121  plyco0  26253  elply2  26257  plypf1  26273  dgreq0  26326  elqaalem2  26385  aalioulem6  26402  aaliou  26403  aaliou2b  26406  ulmss  26461  ulmcn  26463  pserulm  26486  lgamgulmlem5  27098  basellem4  27149  fsumdvdsdiaglem  27248  mpodvdsmulf1o  27259  dvdsmulf1o  27261  chtublem  27276  fsumvma2  27279  logfaclbnd  27287  dchrelbasd  27304  lgsqrlem2  27412  gausslemma2dlem1a  27430  lgseisenlem2  27441  lgsquadlem1  27445  lgsquadlem2  27446  lgsquadlem3  27447  rplogsumlem2  27550  rpvmasumlem  27552  dchrmusum2  27559  dchrvmasumlem1  27560  dchrvmasum2lem  27561  rpvmasum2  27577  dchrisum0lem1  27581  logsqvma  27607  selberg4  27626  pntibndlem3  27657  pntlem3  27674  ostthlem1  27692  ostthlem2  27693  ltsres  27727  nogt01o  27761  oldbdayim  27983  addsproplem2  28064  negsproplem2  28123  mulsval  28203  om2noseqrdg  28398  noseqrdgfn  28400  zmulscld  28491  recut  28588  idmot  28707  brcgr  29102  brbtwn2  29107  axsegconlem8  29126  axpaschlem  29142  axeuclid  29165  axcontlem2  29167  axcontlem7  29172  eengtrkg  29188  upgrex  29294  subgrprop3  29478  subupgr  29489  nbgr0edglem  29558  nb3grprlem1  29582  cusgredg  29626  cusgrres  29650  usgredgsscusgredg  29661  finsumvtxdg2ssteplem4  29750  finsumvtxdg2sstep  29751  wlkl1loop  29839  wlkp1lem4  29876  wwlksnred  30093  wwlksnext  30094  wwlksnextwrd  30098  wpthswwlks2on  30165  clwwlknp  30240  clwwlkel  30249  wwlksext2clwwlk  30260  clwwlknonwwlknonb  30309  3wlkond  30374  1conngr  30397  eucrctshift  30446  fusgr2wsp2nb  30537  numclwwlk1lem2foa  30557  numclwwlk1lem2f1  30560  numclwlk1lem1  30572  numclwlk1lem2  30573  grpoidinvlem1  30708  grporcan  30722  ipblnfi  31059  hvmulcan2  31277  shscli  31521  spansneleq  31774  pjspansn  31781  3oalem2  31867  eigposi  32040  cnlnadjlem2  32272  stlesi  32445  mdslmd1lem1  32529  mdslmd1lem2  32530  cdj1i  32637  disjxpin  32789  nn0xmulclb  32974  xreceu  33100  txomap  34132  pstmxmet  34195  qqhghm  34286  qqhrhm  34287  measinblem  34518  cntmeas  34524  ballotlemsf1o  34812  bnj945  35070  bnj1110  35278  f1resveqaeq  35380  rankfilimbi  35398  cvmopnlem  35629  cvmfolem  35630  cvmliftmolem2  35633  cvmlift2lem10  35663  satf00  35725  satffunlem2lem1  35755  satefvfmla0  35769  mrsubvrs  35873  wzel  36173  btwnconn1lem8  36445  btwnconn1lem9  36446  btwnconn1lem10  36447  btwnconn1lem11  36448  btwnconn1lem12  36449  finminlem  36679  nn0prpwlem  36683  fnessref  36718  refssfne  36719  fnemeet2  36728  consym1  36781  bj-finsumval0  37778  topdifinffinlem  37842  relowlssretop  37858  rdgeqoa  37865  fvineqsneu  37906  pibt2  37912  matunitlindflem1  38116  poimirlem28  38148  mblfinlem1  38157  mblfinlem3  38159  mblfinlem4  38160  ovoliunnfl  38162  mbfresfi  38166  mbfposadd  38167  itg2addnclem2  38172  itg2addnc  38174  ftc1anc  38201  frinfm  38235  fdc  38245  blssp  38256  sstotbnd  38275  isbnd2  38283  ssbnd  38288  prdstotbnd  38294  prdsbnd2  38295  ismtyres  38308  heibor1lem  38309  rrnequiv  38335  rngoisocnv  38481  crngohomfo  38506  pridlc3  38573  membpartlem19  39414  prter3  39507  ax12eq  39566  ax12el  39567  cvratlem  40046  islvol2aN  40217  4atlem4b  40225  4atlem4c  40226  4atlem4d  40227  isline2  40399  isline3  40401  pclfinclN  40575  linepsubclN  40576  pexmidlem4N  40598  diaglbN  41680  dvhvaddcl  41720  dvhvaddcomN  41721  dvhvscacl  41728  djavalN  41760  dibglbN  41791  dihatexv  41963  djhval  42023  mapdrvallem2  42270  evlselvlem  43171  evlselv  43172  mhpind  43177  prjsprellsp  43194  elrfi  43276  nacsfix  43294  eldioph2  43344  lzenom  43352  rexrabdioph  43372  irrapxlem3  43402  pellexlem5  43411  pellex  43413  pell1234qrne0  43431  pell1234qrmulcl  43433  pell14qrdich  43447  pell1qrge1  43448  pellqrex  43457  rmxypairf1o  43489  rmxycomplete  43495  monotoddzzfi  43520  congadd  43544  jm2.19lem3  43569  jm2.19lem4  43570  jm2.25  43577  jm2.26a  43578  jm2.26lem3  43579  expdiophlem1  43599  wepwsolem  43620  lmhmfgsplit  43664  aaitgo  43740  mon1psubm  43777  deg1mhm  43778  succlg  43906  ofoacom  43939  iunrelexp0  44279  isotone2  44626  mnuprdlem4  44852  relpmin  45529  disjrnmpt2  45767  mullimc  46193  mullimcf  46200  climxrre  46325  fprodcncf  46475  stoweidlem17  46592  stoweidlem27  46602  stoweidlem54  46629  fourierdlem42  46724  fourierdlem62  46743  fourierdlem73  46754  fourierdlem76  46757  fourierdlem97  46778  sge0iunmptlemfi  46988  isomenndlem  47105  imarnf1pr  47877  smonoord  47972  fvelsetpreimafv  47994  iccpartiltu  48029  sprsymrelf1lem  48098  prproropf1olem3  48112  paireqne  48118  fmtnoprmfac1  48175  prmdvdsfmtnof1lem2  48195  nprmdvdsfacm1  48234  gricushgr  48540  grimedg  48558  cycl3grtri  48570  gpgedg2iv  48690  pgnbgreunbgrlem2lem1  48737  pgnbgreunbgrlem2lem2  48738  rngcinvALTV  48899  funcringcsetcALTV2lem9  48921  ringcinvALTV  48933  funcringcsetclem9ALTV  48944  lmodvsmdi  49002  lincsum  49052  lindslinindimp2lem4  49084  nn0sumshdiglemB  49243  1arymaptf1  49265  2arymaptf1  49276  dmrnxp  49459  xpco2  49479  initopropd  49865  termopropd  49866  zeroopropd  49867  oduoppcciso  50188  lanpropd  50237  ranpropd  50238