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  3851  f1oprg  5616  fvco4  5705  nnsucuniel  6639  mapen  7003  mapxpen  7005  fidceq  7027  fidifsnen  7028  php5fin  7040  findcard2d  7049  findcard2sd  7050  diffisn  7051  fidcenumlemr  7118  supmoti  7156  djuf1olem  7216  nninfwlpor  7337  exmidfodomrlemim  7375  cc4f  7451  cc4n  7453  subhalfnqq  7597  nqnq0pi  7621  genprndl  7704  genprndu  7705  addlocpr  7719  nqprl  7734  nqpru  7735  addnqprlemrl  7740  addnqprlemru  7741  mullocpr  7754  mulnqprlemrl  7756  mulnqprlemru  7757  ltaprlem  7801  aptiprleml  7822  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  caucvgprlemladdfu  7860  caucvgprprlemloc  7886  suplocexprlemrl  7900  suplocexprlemru  7902  mulcmpblnrlemg  7923  recexgt0sr  7956  pitonn  8031  rereceu  8072  rimul  8728  receuap  8812  peano5uzti  9551  iooshf  10144  seq3fveq2  10692  seqfveq2g  10694  seq3id2  10743  seqfeq3  10746  expcl2lemap  10768  mulexpzap  10796  expnlbnd2  10882  hashfacen  11053  fstwrdne0  11106  swrdsb0eq  11192  swrdswrd  11232  wrd2ind  11250  swrdccatin1  11252  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  absexpzap  11586  fsumf1o  11896  fisum0diag2  11953  fsummulc2  11954  fprodmul  12097  fprodrev  12125  moddvds  12305  dvdsflip  12357  dfgcd3  12526  dfgcd2  12530  lcmgcdlem  12594  cncongr1  12620  hashgcdlem  12755  phisum  12758  pcval  12814  pcqcl  12824  pcid  12842  pcneg  12843  prmpwdvds  12873  pockthg  12875  4sqlem2  12907  4sqlem11  12919  setscom  13067  qusval  13351  mulgdirlem  13685  mulgass  13691  0nsg  13746  ghmmulg  13788  islmodd  14251  lmodvsmmulgdi  14281  islss3  14337  znf1o  14609  tgcl  14732  epttop  14758  cnpnei  14887  txcn  14943  txdis1cn  14946  imasnopn  14967  hmeoimaf1o  14982  txhmeo  14987  metss2lem  15165  bdxmet  15169  bdmopn  15172  metrest  15174  xmetxp  15175  metcnp  15180  dvmptfsum  15393  plycn  15430  dvply2g  15434  rprelogbmul  15623  logbgcd1irr  15635  mpodvdsmulf1o  15658  gausslemma2dlem1a  15731  lgseisenlem2  15744  lgsquadlemsfi  15748  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752