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  3815  f1oprg  5566  fvco4  5651  nnsucuniel  6581  mapen  6943  mapxpen  6945  fidceq  6966  fidifsnen  6967  php5fin  6979  findcard2d  6988  findcard2sd  6989  diffisn  6990  fidcenumlemr  7057  supmoti  7095  djuf1olem  7155  nninfwlpor  7276  exmidfodomrlemim  7309  cc4f  7381  cc4n  7383  subhalfnqq  7527  nqnq0pi  7551  genprndl  7634  genprndu  7635  addlocpr  7649  nqprl  7664  nqpru  7665  addnqprlemrl  7670  addnqprlemru  7671  mullocpr  7684  mulnqprlemrl  7686  mulnqprlemru  7687  ltaprlem  7731  aptiprleml  7752  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  caucvgprlemladdfu  7790  caucvgprprlemloc  7816  suplocexprlemrl  7830  suplocexprlemru  7832  mulcmpblnrlemg  7853  recexgt0sr  7886  pitonn  7961  rereceu  8002  rimul  8658  receuap  8742  peano5uzti  9481  iooshf  10074  seq3fveq2  10620  seqfveq2g  10622  seq3id2  10671  seqfeq3  10674  expcl2lemap  10696  mulexpzap  10724  expnlbnd2  10810  hashfacen  10981  fstwrdne0  11033  swrdsb0eq  11118  absexpzap  11391  fsumf1o  11701  fisum0diag2  11758  fsummulc2  11759  fprodmul  11902  fprodrev  11930  moddvds  12110  dvdsflip  12162  dfgcd3  12331  dfgcd2  12335  lcmgcdlem  12399  cncongr1  12425  hashgcdlem  12560  phisum  12563  pcval  12619  pcqcl  12629  pcid  12647  pcneg  12648  prmpwdvds  12678  pockthg  12680  4sqlem2  12712  4sqlem11  12724  setscom  12872  qusval  13155  mulgdirlem  13489  mulgass  13495  0nsg  13550  ghmmulg  13592  islmodd  14055  lmodvsmmulgdi  14085  islss3  14141  znf1o  14413  tgcl  14536  epttop  14562  cnpnei  14691  txcn  14747  txdis1cn  14750  imasnopn  14771  hmeoimaf1o  14786  txhmeo  14791  metss2lem  14969  bdxmet  14973  bdmopn  14976  metrest  14978  xmetxp  14979  metcnp  14984  dvmptfsum  15197  plycn  15234  dvply2g  15238  rprelogbmul  15427  logbgcd1irr  15439  mpodvdsmulf1o  15462  gausslemma2dlem1a  15535  lgseisenlem2  15548  lgsquadlemsfi  15552  lgsquadlem1  15554  lgsquadlem2  15555  lgsquadlem3  15556