Theorem ad2antll 407

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	|- (ph -> ps)

Assertion

Ref	Expression
ad2antll	|- ((ch /\ (th /\ ph)) -> ps)

Proof of Theorem ad2antll

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- (ph -> ps)
2	1	adantl 388	. 2 |- ((th /\ ph) -> ps)
3	2	adantl 388	1 |- ((ch /\ (th /\ ph)) -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  simprr 415  ax11eq 1363  ax11el 1364  ordsucelsuc 3073  funfvima3 3854  isomin 3899  oalimcl 4194  odi 4210  pw2en 4446  rankxplim3 4714  axacndlem5 4963  axacnd 4964  uzwo4OLD 6210  uzwo 6455  uzwoOLD 6456  recexpt 6595  replimt 6761  climaddlem3 7116  climmullem4 7123  fsum0diaglem2 7257  tgclt 7624  tgss2t 7637  neindisj 7731  dnsconst 7788  opni3 7866  lmcau 7996  grpidinvlem1 8048  grprcan 8063  sspval 8382  ubthlem3 8531  ubthlem4 8532  ubthlem12 8540  minveclem31 8575  minveclem32 8576  chocuni 9172  shscl 9281  spansneleq 9493  pjspansnt 9500  osumlem7 9584  3oalem2 9608  eigpos 9762  cnlnadjlem2 10001  stles 10168  mdslmd1lem1 10252  mdslmd1lem2 10253  cdj1 10360  trnij 10637  codcmpd 10680  cmpidb 10708  imonclem 10741  cmpmon 10743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain