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  5851  fcof1o  5919  infnfi  7065  addcomnqg  7579  addassnqg  7580  nqtri3or  7594  ltexnqq  7606  nqnq0pi  7636  nqpnq0nq  7651  nqnq0a  7652  addassnq0lemcl  7659  ltaddpr  7795  ltexprlemloc  7805  addcanprlemu  7813  recexprlem1ssu  7832  aptiprleml  7837  mulcomsrg  7955  mulasssrg  7956  distrsrg  7957  aptisr  7977  mulcnsr  8033  cnegex  8335  muladd  8541  lemul12b  9019  qaddcl  9842  iooshf  10160  elfzomelpfzo  10449  expnegzap  10807  swrdccatin1  11273  setscom  13088  grplmulf1o  13623  lmodfopne  14306  cnpnei  14909  cxplt3  15610  cxple3  15611  umgr2edg  16021