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  3805  f1oprg  5551  fvco4  5636  nnsucuniel  6562  mapen  6916  mapxpen  6918  fidceq  6939  fidifsnen  6940  php5fin  6952  findcard2d  6961  findcard2sd  6962  diffisn  6963  fidcenumlemr  7030  supmoti  7068  djuf1olem  7128  nninfwlpor  7249  exmidfodomrlemim  7282  cc4f  7354  cc4n  7356  subhalfnqq  7500  nqnq0pi  7524  genprndl  7607  genprndu  7608  addlocpr  7622  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  mullocpr  7657  mulnqprlemrl  7659  mulnqprlemru  7660  ltaprlem  7704  aptiprleml  7725  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  caucvgprlemladdfu  7763  caucvgprprlemloc  7789  suplocexprlemrl  7803  suplocexprlemru  7805  mulcmpblnrlemg  7826  recexgt0sr  7859  pitonn  7934  rereceu  7975  rimul  8631  receuap  8715  peano5uzti  9453  iooshf  10046  seq3fveq2  10586  seqfveq2g  10588  seq3id2  10637  seqfeq3  10640  expcl2lemap  10662  mulexpzap  10690  expnlbnd2  10776  hashfacen  10947  fstwrdne0  10993  absexpzap  11264  fsumf1o  11574  fisum0diag2  11631  fsummulc2  11632  fprodmul  11775  fprodrev  11803  moddvds  11983  dvdsflip  12035  dfgcd3  12204  dfgcd2  12208  lcmgcdlem  12272  cncongr1  12298  hashgcdlem  12433  phisum  12436  pcval  12492  pcqcl  12502  pcid  12520  pcneg  12521  prmpwdvds  12551  pockthg  12553  4sqlem2  12585  4sqlem11  12597  setscom  12745  qusval  13027  mulgdirlem  13361  mulgass  13367  0nsg  13422  ghmmulg  13464  islmodd  13927  lmodvsmmulgdi  13957  islss3  14013  znf1o  14285  tgcl  14408  epttop  14434  cnpnei  14563  txcn  14619  txdis1cn  14622  imasnopn  14643  hmeoimaf1o  14658  txhmeo  14663  metss2lem  14841  bdxmet  14845  bdmopn  14848  metrest  14850  xmetxp  14851  metcnp  14856  dvmptfsum  15069  plycn  15106  dvply2g  15110  rprelogbmul  15299  logbgcd1irr  15311  mpodvdsmulf1o  15334  gausslemma2dlem1a  15407  lgseisenlem2  15420  lgsquadlemsfi  15424  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428