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  533  simprrl  541  simprrr  542  dn1dc  969  prneimg  3862  f1oprg  5638  fvco4  5727  nnsucuniel  6706  modom  7037  mapen  7075  mapxpen  7077  fidceq  7099  fidifsnen  7100  php5fin  7114  findcard2d  7123  findcard2sd  7124  diffisn  7125  fidcenumlemr  7197  supmoti  7235  djuf1olem  7295  nninfwlpor  7416  exmidfodomrlemim  7455  cc4f  7531  cc4n  7533  subhalfnqq  7677  nqnq0pi  7701  genprndl  7784  genprndu  7785  addlocpr  7799  nqprl  7814  nqpru  7815  addnqprlemrl  7820  addnqprlemru  7821  mullocpr  7834  mulnqprlemrl  7836  mulnqprlemru  7837  ltaprlem  7881  aptiprleml  7902  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  caucvgprlemladdfu  7940  caucvgprprlemloc  7966  suplocexprlemrl  7980  suplocexprlemru  7982  mulcmpblnrlemg  8003  recexgt0sr  8036  pitonn  8111  rereceu  8152  rimul  8807  receuap  8891  peano5uzti  9632  iooshf  10231  seq3fveq2  10783  seqfveq2g  10785  seq3id2  10834  seqfeq3  10837  expcl2lemap  10859  mulexpzap  10887  expnlbnd2  10973  hashfacen  11146  fstwrdne0  11202  swrdsb0eq  11295  swrdswrd  11335  wrd2ind  11353  swrdccatin1  11355  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  absexpzap  11703  fsumf1o  12014  fisum0diag2  12071  fsummulc2  12072  fprodmul  12215  fprodrev  12243  moddvds  12423  dvdsflip  12475  dfgcd3  12644  dfgcd2  12648  lcmgcdlem  12712  cncongr1  12738  hashgcdlem  12873  phisum  12876  pcval  12932  pcqcl  12942  pcid  12960  pcneg  12961  prmpwdvds  12991  pockthg  12993  4sqlem2  13025  4sqlem11  13037  setscom  13185  qusval  13469  mulgdirlem  13803  mulgass  13809  0nsg  13864  ghmmulg  13906  islmodd  14372  lmodvsmmulgdi  14402  islss3  14458  znf1o  14730  tgcl  14858  epttop  14884  cnpnei  15013  txcn  15069  txdis1cn  15072  imasnopn  15093  hmeoimaf1o  15108  txhmeo  15113  metss2lem  15291  bdxmet  15295  bdmopn  15298  metrest  15300  xmetxp  15301  metcnp  15306  dvmptfsum  15519  plycn  15556  dvply2g  15560  rprelogbmul  15749  logbgcd1irr  15761  mpodvdsmulf1o  15787  gausslemma2dlem1a  15860  lgseisenlem2  15873  lgsquadlemsfi  15877  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  subgrprop3  16186  subupgr  16197  wlkl1loop  16282  clwwlknp  16341