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  5685  fvco4  5777  nnsucuniel  6768  modom  7108  mapen  7146  mapxpen  7148  mapunen  7151  fidceq  7171  fidifsnen  7172  php5fin  7186  findcard2d  7195  findcard2sd  7196  diffisn  7197  fidcenumlemr  7272  supmoti  7333  djuf1olem  7393  nninfwlpor  7514  exmidfodomrlemim  7553  cc4f  7635  cc4n  7637  subhalfnqq  7781  nqnq0pi  7805  genprndl  7888  genprndu  7889  addlocpr  7903  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  mullocpr  7938  mulnqprlemrl  7940  mulnqprlemru  7941  ltaprlem  7985  aptiprleml  8006  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemladdfu  8044  caucvgprprlemloc  8070  suplocexprlemrl  8084  suplocexprlemru  8086  mulcmpblnrlemg  8107  recexgt0sr  8140  pitonn  8215  rereceu  8256  rimul  8915  receuap  9001  peano5uzti  9758  iooshf  10364  seq3fveq2  10925  seqfveq2g  10927  seq3id2  10976  seqfeq3  10979  expcl2lemap  11001  mulexpzap  11029  expnlbnd2  11116  hashfacen  11298  hashf1lem1  11299  fstwrdne0  11358  swrdsb0eq  11451  swrdswrd  11491  wrd2ind  11509  swrdccatin1  11511  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  absexpzap  11861  fsumf1o  12173  fisum0diag2  12230  fsummulc2  12231  fprodmul  12374  fprodrev  12402  moddvds  12582  dvdsflip  12634  dfgcd3  12803  dfgcd2  12807  lcmgcdlem  12871  cncongr1  12897  hashgcdlem  13036  phisum  13039  pcval  13095  pcqcl  13105  pcid  13123  pcneg  13124  prmpwdvds  13154  pockthg  13156  4sqlem2  13188  4sqlem11  13200  ballotfilemsf1o  13306  setscom  13441  qusval  13693  mulgdirlem  14005  mulgass  14011  0nsg  14066  ghmmulg  14108  islmodd  14678  lmodvsmmulgdi  14709  islss3  14765  znf1o  15035  tgcl  15214  epttop  15240  cnpnei  15369  txcn  15425  txdis1cn  15428  imasnopn  15449  hmeoimaf1o  15464  txhmeo  15469  metss2lem  15647  bdxmet  15651  bdmopn  15654  metrest  15656  xmetxp  15657  metcnp  15662  dvmptfsum  15875  plycn  15912  dvply2g  15916  rprelogbmul  16110  logbgcd1irr  16122  mpodvdsmulf1o  16185  gausslemma2dlem1a  16275  lgseisenlem2  16288  lgsquadlemsfi  16292  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  subgrprop3  16601  subupgr  16612  wlkl1loop  16697  clwwlknp  16756