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  3855  f1oprg  5625  fvco4  5714  nnsucuniel  6658  modom  6989  mapen  7027  mapxpen  7029  fidceq  7051  fidifsnen  7052  php5fin  7064  findcard2d  7073  findcard2sd  7074  diffisn  7075  fidcenumlemr  7145  supmoti  7183  djuf1olem  7243  nninfwlpor  7364  exmidfodomrlemim  7402  cc4f  7478  cc4n  7480  subhalfnqq  7624  nqnq0pi  7648  genprndl  7731  genprndu  7732  addlocpr  7746  nqprl  7761  nqpru  7762  addnqprlemrl  7767  addnqprlemru  7768  mullocpr  7781  mulnqprlemrl  7783  mulnqprlemru  7784  ltaprlem  7828  aptiprleml  7849  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  caucvgprlemladdfu  7887  caucvgprprlemloc  7913  suplocexprlemrl  7927  suplocexprlemru  7929  mulcmpblnrlemg  7950  recexgt0sr  7983  pitonn  8058  rereceu  8099  rimul  8755  receuap  8839  peano5uzti  9578  iooshf  10177  seq3fveq2  10727  seqfveq2g  10729  seq3id2  10778  seqfeq3  10781  expcl2lemap  10803  mulexpzap  10831  expnlbnd2  10917  hashfacen  11090  fstwrdne0  11143  swrdsb0eq  11236  swrdswrd  11276  wrd2ind  11294  swrdccatin1  11296  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  absexpzap  11631  fsumf1o  11941  fisum0diag2  11998  fsummulc2  11999  fprodmul  12142  fprodrev  12170  moddvds  12350  dvdsflip  12402  dfgcd3  12571  dfgcd2  12575  lcmgcdlem  12639  cncongr1  12665  hashgcdlem  12800  phisum  12803  pcval  12859  pcqcl  12869  pcid  12887  pcneg  12888  prmpwdvds  12918  pockthg  12920  4sqlem2  12952  4sqlem11  12964  setscom  13112  qusval  13396  mulgdirlem  13730  mulgass  13736  0nsg  13791  ghmmulg  13833  islmodd  14297  lmodvsmmulgdi  14327  islss3  14383  znf1o  14655  tgcl  14778  epttop  14804  cnpnei  14933  txcn  14989  txdis1cn  14992  imasnopn  15013  hmeoimaf1o  15028  txhmeo  15033  metss2lem  15211  bdxmet  15215  bdmopn  15218  metrest  15220  xmetxp  15221  metcnp  15226  dvmptfsum  15439  plycn  15476  dvply2g  15480  rprelogbmul  15669  logbgcd1irr  15681  mpodvdsmulf1o  15704  gausslemma2dlem1a  15777  lgseisenlem2  15790  lgsquadlemsfi  15794  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  wlkl1loop  16155  clwwlknp  16212