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 1361  ax11el 1362  ordsucelsuc 3068  funfvima3 3845  isomin 3890  oalimcl 4184  odi 4200  pw2en 4432  rankxplim3 4694  axacndlem5 4943  axacnd 4944  ltmul12it 5805  uzwo4OLD 6166  uzwo 6395  uzwoOLD 6396  recexpt 6534  replimt 6700  climaddlem3 7060  climmullem4 7067  fsum0diaglem2 7200  tgclt 7574  tgss2t 7587  neindisj 7681  dnsconst 7738  opni3 7818  lmcau 7946  grpidinvlem1 7998  grprcan 8013  sspval 8329  ubthlem3 8475  ubthlem4 8476  ubthlem12 8484  minveclem31 8519  minveclem32 8520  chocuni 9111  shscl 9219  spansneleq 9432  spansneleqOLD 9433  pjspansnt 9440  osumlem7 9524  3oalem2 9548  eigpos 9702  cnlnadjlem2 9939  stles 10106  mdslmd1lem1 10189  mdslmd1lem2 10190  cdj1 10294  trnij 10517  codcmpd 10560  cmpidb 10588  imonclem 10619  cmpmon 10621

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