Theorem ad2ant2rl 511

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

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

Proof of Theorem ad2ant2rl

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrl 478	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantlr 477	1 |- ( ( ( ph /\ th ) /\ ( ta /\ ps ) ) -> ch )

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:  fvtp1g  5894  fcof1o  5964  infnfi  7154  addcomnqg  7698  addassnqg  7699  nqtri3or  7713  ltexnqq  7725  nqnq0pi  7755  nqpnq0nq  7770  nqnq0a  7771  addassnq0lemcl  7778  ltaddpr  7914  ltexprlemloc  7924  addcanprlemu  7932  recexprlem1ssu  7951  aptiprleml  7956  mulcomsrg  8074  mulasssrg  8075  distrsrg  8076  aptisr  8096  mulcnsr  8152  cnegex  8453  muladd  8659  lemul12b  9137  qaddcl  9970  iooshf  10288  elfzomelpfzo  10580  expnegzap  10939  swrdccatin1  11421  setscom  13269  grplmulf1o  13804  lmodfopne  14491  cnpnei  15101  cxplt3  15802  cxple3  15803  umgr2edg  16219