Theorem ad2antll 495

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 ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simprr  537  simprrl  545  simprrr  546  dn1dc  973  prneimg  3899  f1oprg  5688  fvco4  5780  nnsucuniel  6773  modom  7114  mapen  7152  mapxpen  7154  mapunen  7157  fidceq  7177  fidifsnen  7178  php5fin  7192  findcard2d  7201  findcard2sd  7202  diffisn  7203  fidcenumlemr  7279  supmoti  7339  djuf1olem  7399  nninfwlpor  7520  exmidfodomrlemim  7559  cc4f  7641  cc4n  7643  subhalfnqq  7787  nqnq0pi  7811  genprndl  7894  genprndu  7895  addlocpr  7909  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  mullocpr  7944  mulnqprlemrl  7946  mulnqprlemru  7947  ltaprlem  7991  aptiprleml  8012  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemladdfu  8050  caucvgprprlemloc  8076  suplocexprlemrl  8090  suplocexprlemru  8092  mulcmpblnrlemg  8113  recexgt0sr  8146  pitonn  8221  rereceu  8262  rimul  8921  receuap  9007  peano5uzti  9764  iooshf  10370  seq3fveq2  10932  seqfveq2g  10934  seq3id2  10983  seqfeq3  10986  expcl2lemap  11008  mulexpzap  11036  expnlbnd2  11123  hashfacen  11305  hashf1lem1  11306  fstwrdne0  11365  swrdsb0eq  11458  swrdswrd  11498  wrd2ind  11516  swrdccatin1  11518  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  absexpzap  11868  fsumf1o  12181  fisum0diag2  12238  fsummulc2  12239  fprodmul  12382  fprodrev  12410  moddvds  12590  dvdsflip  12642  dfgcd3  12811  dfgcd2  12815  lcmgcdlem  12879  cncongr1  12905  hashgcdlem  13044  phisum  13047  pcval  13103  pcqcl  13113  pcid  13131  pcneg  13132  prmpwdvds  13162  pockthg  13164  4sqlem2  13196  4sqlem11  13208  ballotfilemsf1o  13314  setscom  13449  qusval  13702  mulgdirlem  14014  mulgass  14020  0nsg  14075  ghmmulg  14117  islmodd  14737  lmodvsmmulgdi  14768  islss3  14824  znf1o  15094  tgcl  15307  epttop  15333  cnpnei  15462  txcn  15518  txdis1cn  15521  imasnopn  15542  hmeoimaf1o  15557  txhmeo  15562  metss2lem  15740  bdxmet  15744  bdmopn  15747  metrest  15749  xmetxp  15750  metcnp  15755  dvmptfsum  15968  plycn  16005  dvply2g  16009  rprelogbmul  16208  logbgcd1irr  16220  mpodvdsmulf1o  16301  chtublem  16312  gausslemma2dlem1a  16399  lgseisenlem2  16412  lgsquadlemsfi  16416  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  subgrprop3  16725  subupgr  16736  wlkl1loop  16821  clwwlknp  16880