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  5847  fcof1o  5913  infnfi  7057  addcomnqg  7568  addassnqg  7569  nqtri3or  7583  ltexnqq  7595  nqnq0pi  7625  nqpnq0nq  7640  nqnq0a  7641  addassnq0lemcl  7648  ltaddpr  7784  ltexprlemloc  7794  addcanprlemu  7802  recexprlem1ssu  7821  aptiprleml  7826  mulcomsrg  7944  mulasssrg  7945  distrsrg  7946  aptisr  7966  mulcnsr  8022  cnegex  8324  muladd  8530  lemul12b  9008  qaddcl  9830  iooshf  10148  elfzomelpfzo  10437  expnegzap  10795  swrdccatin1  11257  setscom  13072  grplmulf1o  13607  lmodfopne  14290  cnpnei  14893  cxplt3  15594  cxple3  15595  umgr2edg  16005