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  966  prneimg  3852  f1oprg  5619  fvco4  5708  nnsucuniel  6649  mapen  7015  mapxpen  7017  fidceq  7039  fidifsnen  7040  php5fin  7052  findcard2d  7061  findcard2sd  7062  diffisn  7063  fidcenumlemr  7133  supmoti  7171  djuf1olem  7231  nninfwlpor  7352  exmidfodomrlemim  7390  cc4f  7466  cc4n  7468  subhalfnqq  7612  nqnq0pi  7636  genprndl  7719  genprndu  7720  addlocpr  7734  nqprl  7749  nqpru  7750  addnqprlemrl  7755  addnqprlemru  7756  mullocpr  7769  mulnqprlemrl  7771  mulnqprlemru  7772  ltaprlem  7816  aptiprleml  7837  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemladdfu  7875  caucvgprprlemloc  7901  suplocexprlemrl  7915  suplocexprlemru  7917  mulcmpblnrlemg  7938  recexgt0sr  7971  pitonn  8046  rereceu  8087  rimul  8743  receuap  8827  peano5uzti  9566  iooshf  10160  seq3fveq2  10709  seqfveq2g  10711  seq3id2  10760  seqfeq3  10763  expcl2lemap  10785  mulexpzap  10813  expnlbnd2  10899  hashfacen  11071  fstwrdne0  11124  swrdsb0eq  11212  swrdswrd  11252  wrd2ind  11270  swrdccatin1  11272  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  absexpzap  11606  fsumf1o  11916  fisum0diag2  11973  fsummulc2  11974  fprodmul  12117  fprodrev  12145  moddvds  12325  dvdsflip  12377  dfgcd3  12546  dfgcd2  12550  lcmgcdlem  12614  cncongr1  12640  hashgcdlem  12775  phisum  12778  pcval  12834  pcqcl  12844  pcid  12862  pcneg  12863  prmpwdvds  12893  pockthg  12895  4sqlem2  12927  4sqlem11  12939  setscom  13087  qusval  13371  mulgdirlem  13705  mulgass  13711  0nsg  13766  ghmmulg  13808  islmodd  14272  lmodvsmmulgdi  14302  islss3  14358  znf1o  14630  tgcl  14753  epttop  14779  cnpnei  14908  txcn  14964  txdis1cn  14967  imasnopn  14988  hmeoimaf1o  15003  txhmeo  15008  metss2lem  15186  bdxmet  15190  bdmopn  15193  metrest  15195  xmetxp  15196  metcnp  15201  dvmptfsum  15414  plycn  15451  dvply2g  15455  rprelogbmul  15644  logbgcd1irr  15656  mpodvdsmulf1o  15679  gausslemma2dlem1a  15752  lgseisenlem2  15765  lgsquadlemsfi  15769  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  wlkl1loop  16099