Theorem ad2ant2rl 500

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  fvtp1g  5582  fcof1o  5644  infnfi  6742  addcomnqg  7134  addassnqg  7135  nqtri3or  7149  ltexnqq  7161  nqnq0pi  7191  nqpnq0nq  7206  nqnq0a  7207  addassnq0lemcl  7214  ltaddpr  7350  ltexprlemloc  7360  addcanprlemu  7368  recexprlem1ssu  7387  aptiprleml  7392  mulcomsrg  7497  mulasssrg  7498  distrsrg  7499  aptisr  7518  mulcnsr  7567  cnegex  7860  muladd  8062  lemul12b  8526  qaddcl  9326  iooshf  9625  elfzomelpfzo  9898  expnegzap  10217  setscom  11839  cnpnei  12227