Theorem ad2antll 491

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simprr  531  simprrl  539  simprrr  540  dn1dc  963  prneimg  3828  f1oprg  5589  fvco4  5674  nnsucuniel  6604  mapen  6968  mapxpen  6970  fidceq  6992  fidifsnen  6993  php5fin  7005  findcard2d  7014  findcard2sd  7015  diffisn  7016  fidcenumlemr  7083  supmoti  7121  djuf1olem  7181  nninfwlpor  7302  exmidfodomrlemim  7340  cc4f  7416  cc4n  7418  subhalfnqq  7562  nqnq0pi  7586  genprndl  7669  genprndu  7670  addlocpr  7684  nqprl  7699  nqpru  7700  addnqprlemrl  7705  addnqprlemru  7706  mullocpr  7719  mulnqprlemrl  7721  mulnqprlemru  7722  ltaprlem  7766  aptiprleml  7787  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  caucvgprlemladdfu  7825  caucvgprprlemloc  7851  suplocexprlemrl  7865  suplocexprlemru  7867  mulcmpblnrlemg  7888  recexgt0sr  7921  pitonn  7996  rereceu  8037  rimul  8693  receuap  8777  peano5uzti  9516  iooshf  10109  seq3fveq2  10657  seqfveq2g  10659  seq3id2  10708  seqfeq3  10711  expcl2lemap  10733  mulexpzap  10761  expnlbnd2  10847  hashfacen  11018  fstwrdne0  11070  swrdsb0eq  11156  swrdswrd  11196  wrd2ind  11214  swrdccatin1  11216  pfxccatin12  11224  pfxccat3  11225  swrdccat  11226  absexpzap  11506  fsumf1o  11816  fisum0diag2  11873  fsummulc2  11874  fprodmul  12017  fprodrev  12045  moddvds  12225  dvdsflip  12277  dfgcd3  12446  dfgcd2  12450  lcmgcdlem  12514  cncongr1  12540  hashgcdlem  12675  phisum  12678  pcval  12734  pcqcl  12744  pcid  12762  pcneg  12763  prmpwdvds  12793  pockthg  12795  4sqlem2  12827  4sqlem11  12839  setscom  12987  qusval  13270  mulgdirlem  13604  mulgass  13610  0nsg  13665  ghmmulg  13707  islmodd  14170  lmodvsmmulgdi  14200  islss3  14256  znf1o  14528  tgcl  14651  epttop  14677  cnpnei  14806  txcn  14862  txdis1cn  14865  imasnopn  14886  hmeoimaf1o  14901  txhmeo  14906  metss2lem  15084  bdxmet  15088  bdmopn  15091  metrest  15093  xmetxp  15094  metcnp  15099  dvmptfsum  15312  plycn  15349  dvply2g  15353  rprelogbmul  15542  logbgcd1irr  15554  mpodvdsmulf1o  15577  gausslemma2dlem1a  15650  lgseisenlem2  15663  lgsquadlemsfi  15667  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671