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  962  prneimg  3814  f1oprg  5565  fvco4  5650  nnsucuniel  6580  mapen  6942  mapxpen  6944  fidceq  6965  fidifsnen  6966  php5fin  6978  findcard2d  6987  findcard2sd  6988  diffisn  6989  fidcenumlemr  7056  supmoti  7094  djuf1olem  7154  nninfwlpor  7275  exmidfodomrlemim  7308  cc4f  7380  cc4n  7382  subhalfnqq  7526  nqnq0pi  7550  genprndl  7633  genprndu  7634  addlocpr  7648  nqprl  7663  nqpru  7664  addnqprlemrl  7669  addnqprlemru  7670  mullocpr  7683  mulnqprlemrl  7685  mulnqprlemru  7686  ltaprlem  7730  aptiprleml  7751  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  caucvgprlemladdfu  7789  caucvgprprlemloc  7815  suplocexprlemrl  7829  suplocexprlemru  7831  mulcmpblnrlemg  7852  recexgt0sr  7885  pitonn  7960  rereceu  8001  rimul  8657  receuap  8741  peano5uzti  9480  iooshf  10073  seq3fveq2  10618  seqfveq2g  10620  seq3id2  10669  seqfeq3  10672  expcl2lemap  10694  mulexpzap  10722  expnlbnd2  10808  hashfacen  10979  fstwrdne0  11031  absexpzap  11362  fsumf1o  11672  fisum0diag2  11729  fsummulc2  11730  fprodmul  11873  fprodrev  11901  moddvds  12081  dvdsflip  12133  dfgcd3  12302  dfgcd2  12306  lcmgcdlem  12370  cncongr1  12396  hashgcdlem  12531  phisum  12534  pcval  12590  pcqcl  12600  pcid  12618  pcneg  12619  prmpwdvds  12649  pockthg  12651  4sqlem2  12683  4sqlem11  12695  setscom  12843  qusval  13126  mulgdirlem  13460  mulgass  13466  0nsg  13521  ghmmulg  13563  islmodd  14026  lmodvsmmulgdi  14056  islss3  14112  znf1o  14384  tgcl  14507  epttop  14533  cnpnei  14662  txcn  14718  txdis1cn  14721  imasnopn  14742  hmeoimaf1o  14757  txhmeo  14762  metss2lem  14940  bdxmet  14944  bdmopn  14947  metrest  14949  xmetxp  14950  metcnp  14955  dvmptfsum  15168  plycn  15205  dvply2g  15209  rprelogbmul  15398  logbgcd1irr  15410  mpodvdsmulf1o  15433  gausslemma2dlem1a  15506  lgseisenlem2  15519  lgsquadlemsfi  15523  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527