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  533  simprrl  541  simprrr  542  dn1dc  969  prneimg  3883  f1oprg  5665  fvco4  5754  nnsucuniel  6741  modom  7074  mapen  7112  mapxpen  7114  mapunen  7117  fidceq  7137  fidifsnen  7138  php5fin  7152  findcard2d  7161  findcard2sd  7162  diffisn  7163  fidcenumlemr  7238  supmoti  7297  djuf1olem  7357  nninfwlpor  7478  exmidfodomrlemim  7517  cc4f  7599  cc4n  7601  subhalfnqq  7745  nqnq0pi  7769  genprndl  7852  genprndu  7853  addlocpr  7867  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  mullocpr  7902  mulnqprlemrl  7904  mulnqprlemru  7905  ltaprlem  7949  aptiprleml  7970  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  caucvgprlemladdfu  8008  caucvgprprlemloc  8034  suplocexprlemrl  8048  suplocexprlemru  8050  mulcmpblnrlemg  8071  recexgt0sr  8104  pitonn  8179  rereceu  8220  rimul  8876  receuap  8960  peano5uzti  9704  iooshf  10304  seq3fveq2  10861  seqfveq2g  10863  seq3id2  10912  seqfeq3  10915  expcl2lemap  10937  mulexpzap  10965  expnlbnd2  11052  hashfacen  11233  fstwrdne0  11289  swrdsb0eq  11382  swrdswrd  11422  wrd2ind  11440  swrdccatin1  11442  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  absexpzap  11790  fsumf1o  12101  fisum0diag2  12158  fsummulc2  12159  fprodmul  12302  fprodrev  12330  moddvds  12510  dvdsflip  12562  dfgcd3  12731  dfgcd2  12735  lcmgcdlem  12799  cncongr1  12825  hashgcdlem  12960  phisum  12963  pcval  13019  pcqcl  13029  pcid  13047  pcneg  13048  prmpwdvds  13078  pockthg  13080  4sqlem2  13112  4sqlem11  13124  ballotfilemsf1o  13201  setscom  13336  qusval  13587  mulgdirlem  13906  mulgass  13912  0nsg  13967  ghmmulg  14009  islmodd  14567  lmodvsmmulgdi  14597  islss3  14653  znf1o  14925  tgcl  15055  epttop  15081  cnpnei  15210  txcn  15266  txdis1cn  15269  imasnopn  15290  hmeoimaf1o  15305  txhmeo  15310  metss2lem  15488  bdxmet  15492  bdmopn  15495  metrest  15497  xmetxp  15498  metcnp  15503  dvmptfsum  15716  plycn  15753  dvply2g  15757  rprelogbmul  15946  logbgcd1irr  15958  mpodvdsmulf1o  15984  gausslemma2dlem1a  16057  lgseisenlem2  16070  lgsquadlemsfi  16074  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  subgrprop3  16383  subupgr  16394  wlkl1loop  16479  clwwlknp  16538