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  960  prneimg  3770  f1oprg  5497  fvco4  5580  nnsucuniel  6486  mapen  6836  mapxpen  6838  fidceq  6859  fidifsnen  6860  php5fin  6872  findcard2d  6881  findcard2sd  6882  diffisn  6883  fidcenumlemr  6944  supmoti  6982  djuf1olem  7042  nninfwlpor  7162  exmidfodomrlemim  7190  cc4f  7243  cc4n  7245  subhalfnqq  7388  nqnq0pi  7412  genprndl  7495  genprndu  7496  addlocpr  7510  nqprl  7525  nqpru  7526  addnqprlemrl  7531  addnqprlemru  7532  mullocpr  7545  mulnqprlemrl  7547  mulnqprlemru  7548  ltaprlem  7592  aptiprleml  7613  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  caucvgprlemladdfu  7651  caucvgprprlemloc  7677  suplocexprlemrl  7691  suplocexprlemru  7693  mulcmpblnrlemg  7714  recexgt0sr  7747  pitonn  7822  rereceu  7863  rimul  8516  receuap  8599  peano5uzti  9334  iooshf  9923  seq3fveq2  10439  seq3id2  10479  seqfeq3  10482  expcl2lemap  10502  mulexpzap  10530  expnlbnd2  10615  hashfacen  10784  absexpzap  11057  fsumf1o  11366  fisum0diag2  11423  fsummulc2  11424  fprodmul  11567  fprodrev  11595  moddvds  11774  dvdsflip  11824  dfgcd3  11978  dfgcd2  11982  lcmgcdlem  12044  cncongr1  12070  hashgcdlem  12205  phisum  12207  pcval  12263  pcqcl  12273  pcid  12290  pcneg  12291  prmpwdvds  12320  pockthg  12322  4sqlem2  12354  setscom  12469  mulgdirlem  12874  mulgass  12880  tgcl  13135  epttop  13161  cnpnei  13290  txcn  13346  txdis1cn  13349  imasnopn  13370  hmeoimaf1o  13385  txhmeo  13390  metss2lem  13568  bdxmet  13572  bdmopn  13575  metrest  13577  xmetxp  13578  metcnp  13583  rprelogbmul  13944  logbgcd1irr  13956