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  5897  fcof1o  5968  infnfi  7165  addcomnqg  7712  addassnqg  7713  nqtri3or  7727  ltexnqq  7739  nqnq0pi  7769  nqpnq0nq  7784  nqnq0a  7785  addassnq0lemcl  7792  ltaddpr  7928  ltexprlemloc  7938  addcanprlemu  7946  recexprlem1ssu  7965  aptiprleml  7970  mulcomsrg  8088  mulasssrg  8089  distrsrg  8090  aptisr  8110  mulcnsr  8166  cnegex  8467  muladd  8674  lemul12b  9152  qaddcl  9985  iooshf  10304  elfzomelpfzo  10598  expnegzap  10959  swrdccatin1  11442  setscom  13336  grplmulf1o  13829  lmodfopne  14600  cnpnei  15210  cxplt3  15911  cxple3  15912  umgr2edg  16328