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  5794  fcof1o  5860  infnfi  6994  addcomnqg  7496  addassnqg  7497  nqtri3or  7511  ltexnqq  7523  nqnq0pi  7553  nqpnq0nq  7568  nqnq0a  7569  addassnq0lemcl  7576  ltaddpr  7712  ltexprlemloc  7722  addcanprlemu  7730  recexprlem1ssu  7749  aptiprleml  7754  mulcomsrg  7872  mulasssrg  7873  distrsrg  7874  aptisr  7894  mulcnsr  7950  cnegex  8252  muladd  8458  lemul12b  8936  qaddcl  9758  iooshf  10076  elfzomelpfzo  10362  expnegzap  10720  setscom  12905  grplmulf1o  13439  lmodfopne  14121  cnpnei  14724  cxplt3  15425  cxple3  15426