Theorem ad2ant2rl 503

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 470	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantlr 469	1 |- ( ( ( ph /\ th ) /\ ( ta /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  fvtp1g  5693  fcof1o  5757  infnfi  6861  addcomnqg  7322  addassnqg  7323  nqtri3or  7337  ltexnqq  7349  nqnq0pi  7379  nqpnq0nq  7394  nqnq0a  7395  addassnq0lemcl  7402  ltaddpr  7538  ltexprlemloc  7548  addcanprlemu  7556  recexprlem1ssu  7575  aptiprleml  7580  mulcomsrg  7698  mulasssrg  7699  distrsrg  7700  aptisr  7720  mulcnsr  7776  cnegex  8076  muladd  8282  lemul12b  8756  qaddcl  9573  iooshf  9888  elfzomelpfzo  10166  expnegzap  10489  setscom  12434  cnpnei  12859  cxplt3  13480  cxple3  13481