Theorem ad2antll 478

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 273	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜓)
3	2	adantl 273	1 ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simprr  502  simprrl  509  simprrr  510  dn1dc  912  prneimg  3648  f1oprg  5343  fvco4  5425  nnsucuniel  6321  mapen  6669  mapxpen  6671  fidceq  6692  fidifsnen  6693  php5fin  6705  findcard2d  6714  findcard2sd  6715  diffisn  6716  fidcenumlemr  6771  supmoti  6795  djuf1olem  6853  exmidfodomrlemim  6966  subhalfnqq  7123  nqnq0pi  7147  genprndl  7230  genprndu  7231  addlocpr  7245  nqprl  7260  nqpru  7261  addnqprlemrl  7266  addnqprlemru  7267  mullocpr  7280  mulnqprlemrl  7282  mulnqprlemru  7283  ltaprlem  7327  aptiprleml  7348  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  caucvgprlemladdfu  7386  caucvgprprlemloc  7412  mulcmpblnrlemg  7436  recexgt0sr  7469  pitonn  7535  rereceu  7574  rimul  8213  receuap  8291  peano5uzti  9011  iooshf  9576  seq3fveq2  10083  seq3id2  10123  seqfeq3  10126  expcl2lemap  10146  mulexpzap  10174  expnlbnd2  10258  hashfacen  10420  absexpzap  10692  fsumf1o  10998  fisum0diag2  11055  fsummulc2  11056  moddvds  11297  dvdsflip  11344  dfgcd3  11491  dfgcd2  11495  lcmgcdlem  11551  cncongr1  11577  hashgcdlem  11695  setscom  11781  tgcl  12015  epttop  12041  cnpnei  12169  txcn  12225  txdis1cn  12228  imasnopn  12249  metss2lem  12425  bdxmet  12429  bdmopn  12432  metrest  12434  metcnp  12436