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  5892  fcof1o  5962  infnfi  7152  addcomnqg  7696  addassnqg  7697  nqtri3or  7711  ltexnqq  7723  nqnq0pi  7753  nqpnq0nq  7768  nqnq0a  7769  addassnq0lemcl  7776  ltaddpr  7912  ltexprlemloc  7922  addcanprlemu  7930  recexprlem1ssu  7949  aptiprleml  7954  mulcomsrg  8072  mulasssrg  8073  distrsrg  8074  aptisr  8094  mulcnsr  8150  cnegex  8451  muladd  8657  lemul12b  9135  qaddcl  9967  iooshf  10285  elfzomelpfzo  10576  expnegzap  10935  swrdccatin1  11417  setscom  13252  grplmulf1o  13787  lmodfopne  14474  cnpnei  15084  cxplt3  15785  cxple3  15786  umgr2edg  16202