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  6772  modom  7112  mapen  7150  mapxpen  7152  mapunen  7155  fidceq  7175  fidifsnen  7176  php5fin  7190  findcard2d  7199  findcard2sd  7200  diffisn  7201  fidcenumlemr  7277  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  9765  iooshf  10371  seq3fveq2  10933  seqfveq2g  10935  seq3id2  10984  seqfeq3  10987  expcl2lemap  11009  mulexpzap  11037  expnlbnd2  11124  hashfacen  11306  hashf1lem1  11307  fstwrdne0  11366  swrdsb0eq  11459  swrdswrd  11499  wrd2ind  11517  swrdccatin1  11519  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  absexpzap  11869  fsumf1o  12182  fisum0diag2  12239  fsummulc2  12240  fprodmul  12383  fprodrev  12411  moddvds  12591  dvdsflip  12643  dfgcd3  12812  dfgcd2  12816  lcmgcdlem  12880  cncongr1  12906  hashgcdlem  13045  phisum  13048  pcval  13104  pcqcl  13114  pcid  13132  pcneg  13133  prmpwdvds  13163  pockthg  13165  4sqlem2  13197  4sqlem11  13209  ballotfilemsf1o  13315  setscom  13450  qusval  13703  mulgdirlem  14015  mulgass  14021  0nsg  14076  ghmmulg  14118  islmodd  14738  lmodvsmmulgdi  14769  islss3  14825  znf1o  15095  tgcl  15290  epttop  15316  cnpnei  15445  txcn  15501  txdis1cn  15504  imasnopn  15525  hmeoimaf1o  15540  txhmeo  15545  metss2lem  15723  bdxmet  15727  bdmopn  15730  metrest  15732  xmetxp  15733  metcnp  15738  dvmptfsum  15951  plycn  15988  dvply2g  15992  rprelogbmul  16191  logbgcd1irr  16203  mpodvdsmulf1o  16284  chtublem  16295  gausslemma2dlem1a  16382  lgseisenlem2  16395  lgsquadlemsfi  16399  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  subgrprop3  16708  subupgr  16719  wlkl1loop  16804  clwwlknp  16863