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  7280  cc4f  7352  cc4n  7354  subhalfnqq  7498  nqnq0pi  7522  genprndl  7605  genprndu  7606  addlocpr  7620  nqprl  7635  nqpru  7636  addnqprlemrl  7641  addnqprlemru  7642  mullocpr  7655  mulnqprlemrl  7657  mulnqprlemru  7658  ltaprlem  7702  aptiprleml  7723  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  caucvgprlemladdfu  7761  caucvgprprlemloc  7787  suplocexprlemrl  7801  suplocexprlemru  7803  mulcmpblnrlemg  7824  recexgt0sr  7857  pitonn  7932  rereceu  7973  rimul  8629  receuap  8713  peano5uzti  9451  iooshf  10044  seq3fveq2  10584  seqfveq2g  10586  seq3id2  10635  seqfeq3  10638  expcl2lemap  10660  mulexpzap  10688  expnlbnd2  10774  hashfacen  10945  fstwrdne0  10991  absexpzap  11262  fsumf1o  11572  fisum0diag2  11629  fsummulc2  11630  fprodmul  11773  fprodrev  11801  moddvds  11981  dvdsflip  12033  dfgcd3  12202  dfgcd2  12206  lcmgcdlem  12270  cncongr1  12296  hashgcdlem  12431  phisum  12434  pcval  12490  pcqcl  12500  pcid  12518  pcneg  12519  prmpwdvds  12549  pockthg  12551  4sqlem2  12583  4sqlem11  12595  setscom  12743  qusval  13025  mulgdirlem  13359  mulgass  13365  0nsg  13420  ghmmulg  13462  islmodd  13925  lmodvsmmulgdi  13955  islss3  14011  znf1o  14283  tgcl  14384  epttop  14410  cnpnei  14539  txcn  14595  txdis1cn  14598  imasnopn  14619  hmeoimaf1o  14634  txhmeo  14639  metss2lem  14817  bdxmet  14821  bdmopn  14824  metrest  14826  xmetxp  14827  metcnp  14832  dvmptfsum  15045  plycn  15082  dvply2g  15086  rprelogbmul  15275  logbgcd1irr  15287  mpodvdsmulf1o  15310  gausslemma2dlem1a  15383  lgseisenlem2  15396  lgsquadlemsfi  15400  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404