Theorem ad2ant2rl 495

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  fvtp1g  5505  fcof1o  5568  infnfi  6611  addcomnqg  6940  addassnqg  6941  nqtri3or  6955  ltexnqq  6967  nqnq0pi  6997  nqpnq0nq  7012  nqnq0a  7013  addassnq0lemcl  7020  ltaddpr  7156  ltexprlemloc  7166  addcanprlemu  7174  recexprlem1ssu  7193  aptiprleml  7198  mulcomsrg  7303  mulasssrg  7304  distrsrg  7305  aptisr  7324  mulcnsr  7372  cnegex  7660  muladd  7862  lemul12b  8322  qaddcl  9120  iooshf  9370  elfzomelpfzo  9642  expnegzap  9989  setscom  11534