Theorem ad2antll 416

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 397	. 2 |- ((th /\ ph) -> ps)
3	2	adantl 397	1 |- ((ch /\ (th /\ ph)) -> ps)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  simprr 424  ax11eq 1405  ax11el 1406  ordsucelsuc 3130  funfvima3 3911  isomin 3957  oalimcl 4252  odi 4268  pw2en 4509  rankxplim3 4776  axacndlem5 5028  axacnd 5029  uzwo4OLD 6295  iooshf 6421  uzwo 6481  uzwoOLD 6482  recexp 6684  replim 6851  climaddlem3 7206  climmullem4 7213  fsum0diaglem2 7347  tgcl 7713  tgss2 7726  neindisj 7816  dnsconst 7873  opni3 7951  lmcau 8081  grpidinvlem1 8133  grprcan 8147  sspval 8466  ubthlem3 8615  ubthlem4 8616  ubthlem12 8624  minveclem31 8659  minveclem32 8660  chocunii 9255  shscli 9364  spansneleq 9576  pjspansn 9583  osumlem7 9667  3oalem2 9691  eigposi 9845  cnlnadjlem2 10084  stlesi 10252  mdslmd1lem1 10336  mdslmd1lem2 10337  cdj1i 10444  trnij 10719  codcmpd 10762  cmpidb 10790  imonclem 10823  cmpmon 10825

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 154  df-an 232

Copyright terms: Public domain