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  3800  f1oprg  5544  fvco4  5629  nnsucuniel  6548  mapen  6902  mapxpen  6904  fidceq  6925  fidifsnen  6926  php5fin  6938  findcard2d  6947  findcard2sd  6948  diffisn  6949  fidcenumlemr  7014  supmoti  7052  djuf1olem  7112  nninfwlpor  7233  exmidfodomrlemim  7261  cc4f  7329  cc4n  7331  subhalfnqq  7474  nqnq0pi  7498  genprndl  7581  genprndu  7582  addlocpr  7596  nqprl  7611  nqpru  7612  addnqprlemrl  7617  addnqprlemru  7618  mullocpr  7631  mulnqprlemrl  7633  mulnqprlemru  7634  ltaprlem  7678  aptiprleml  7699  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  caucvgprlemladdfu  7737  caucvgprprlemloc  7763  suplocexprlemrl  7777  suplocexprlemru  7779  mulcmpblnrlemg  7800  recexgt0sr  7833  pitonn  7908  rereceu  7949  rimul  8604  receuap  8688  peano5uzti  9425  iooshf  10018  seq3fveq2  10546  seqfveq2g  10548  seq3id2  10597  seqfeq3  10600  expcl2lemap  10622  mulexpzap  10650  expnlbnd2  10736  hashfacen  10907  fstwrdne0  10953  absexpzap  11224  fsumf1o  11533  fisum0diag2  11590  fsummulc2  11591  fprodmul  11734  fprodrev  11762  moddvds  11942  dvdsflip  11993  dfgcd3  12147  dfgcd2  12151  lcmgcdlem  12215  cncongr1  12241  hashgcdlem  12376  phisum  12378  pcval  12434  pcqcl  12444  pcid  12462  pcneg  12463  prmpwdvds  12493  pockthg  12495  4sqlem2  12527  4sqlem11  12539  setscom  12658  qusval  12906  mulgdirlem  13223  mulgass  13229  0nsg  13284  ghmmulg  13326  islmodd  13789  lmodvsmmulgdi  13819  islss3  13875  znf1o  14139  tgcl  14232  epttop  14258  cnpnei  14387  txcn  14443  txdis1cn  14446  imasnopn  14467  hmeoimaf1o  14482  txhmeo  14487  metss2lem  14665  bdxmet  14669  bdmopn  14672  metrest  14674  xmetxp  14675  metcnp  14680  rprelogbmul  15087  logbgcd1irr  15099  gausslemma2dlem1a  15174  lgseisenlem2  15187  lgsquadlem1  15191