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  3772  f1oprg  5501  fvco4  5584  nnsucuniel  6490  mapen  6840  mapxpen  6842  fidceq  6863  fidifsnen  6864  php5fin  6876  findcard2d  6885  findcard2sd  6886  diffisn  6887  fidcenumlemr  6948  supmoti  6986  djuf1olem  7046  nninfwlpor  7166  exmidfodomrlemim  7194  cc4f  7259  cc4n  7261  subhalfnqq  7404  nqnq0pi  7428  genprndl  7511  genprndu  7512  addlocpr  7526  nqprl  7541  nqpru  7542  addnqprlemrl  7547  addnqprlemru  7548  mullocpr  7561  mulnqprlemrl  7563  mulnqprlemru  7564  ltaprlem  7608  aptiprleml  7629  cauappcvgprlemladdfu  7644  cauappcvgprlemladdfl  7645  caucvgprlemladdfu  7667  caucvgprprlemloc  7693  suplocexprlemrl  7707  suplocexprlemru  7709  mulcmpblnrlemg  7730  recexgt0sr  7763  pitonn  7838  rereceu  7879  rimul  8532  receuap  8615  peano5uzti  9350  iooshf  9939  seq3fveq2  10455  seq3id2  10495  seqfeq3  10498  expcl2lemap  10518  mulexpzap  10546  expnlbnd2  10631  hashfacen  10800  absexpzap  11073  fsumf1o  11382  fisum0diag2  11439  fsummulc2  11440  fprodmul  11583  fprodrev  11611  moddvds  11790  dvdsflip  11840  dfgcd3  11994  dfgcd2  11998  lcmgcdlem  12060  cncongr1  12086  hashgcdlem  12221  phisum  12223  pcval  12279  pcqcl  12289  pcid  12306  pcneg  12307  prmpwdvds  12336  pockthg  12338  4sqlem2  12370  setscom  12485  mulgdirlem  12902  mulgass  12908  tgcl  13231  epttop  13257  cnpnei  13386  txcn  13442  txdis1cn  13445  imasnopn  13466  hmeoimaf1o  13481  txhmeo  13486  metss2lem  13664  bdxmet  13668  bdmopn  13671  metrest  13673  xmetxp  13674  metcnp  13679  rprelogbmul  14040  logbgcd1irr  14052