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  3789  f1oprg  5524  fvco4  5609  nnsucuniel  6521  mapen  6875  mapxpen  6877  fidceq  6898  fidifsnen  6899  php5fin  6911  findcard2d  6920  findcard2sd  6921  diffisn  6922  fidcenumlemr  6985  supmoti  7023  djuf1olem  7083  nninfwlpor  7203  exmidfodomrlemim  7231  cc4f  7299  cc4n  7301  subhalfnqq  7444  nqnq0pi  7468  genprndl  7551  genprndu  7552  addlocpr  7566  nqprl  7581  nqpru  7582  addnqprlemrl  7587  addnqprlemru  7588  mullocpr  7601  mulnqprlemrl  7603  mulnqprlemru  7604  ltaprlem  7648  aptiprleml  7669  cauappcvgprlemladdfu  7684  cauappcvgprlemladdfl  7685  caucvgprlemladdfu  7707  caucvgprprlemloc  7733  suplocexprlemrl  7747  suplocexprlemru  7749  mulcmpblnrlemg  7770  recexgt0sr  7803  pitonn  7878  rereceu  7919  rimul  8573  receuap  8657  peano5uzti  9392  iooshf  9984  seq3fveq2  10502  seq3id2  10542  seqfeq3  10545  expcl2lemap  10566  mulexpzap  10594  expnlbnd2  10680  hashfacen  10851  absexpzap  11124  fsumf1o  11433  fisum0diag2  11490  fsummulc2  11491  fprodmul  11634  fprodrev  11662  moddvds  11841  dvdsflip  11892  dfgcd3  12046  dfgcd2  12050  lcmgcdlem  12112  cncongr1  12138  hashgcdlem  12273  phisum  12275  pcval  12331  pcqcl  12341  pcid  12359  pcneg  12360  prmpwdvds  12390  pockthg  12392  4sqlem2  12424  4sqlem11  12436  setscom  12555  qusval  12803  mulgdirlem  13110  mulgass  13116  0nsg  13170  ghmmulg  13212  islmodd  13626  lmodvsmmulgdi  13656  islss3  13712  tgcl  14041  epttop  14067  cnpnei  14196  txcn  14252  txdis1cn  14255  imasnopn  14276  hmeoimaf1o  14291  txhmeo  14296  metss2lem  14474  bdxmet  14478  bdmopn  14481  metrest  14483  xmetxp  14484  metcnp  14489  rprelogbmul  14850  logbgcd1irr  14862  lgseisenlem2  14929