Theorem ad2ant2rl 502

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 469	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantlr 468	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  5621  fcof1o  5683  infnfi  6782  addcomnqg  7182  addassnqg  7183  nqtri3or  7197  ltexnqq  7209  nqnq0pi  7239  nqpnq0nq  7254  nqnq0a  7255  addassnq0lemcl  7262  ltaddpr  7398  ltexprlemloc  7408  addcanprlemu  7416  recexprlem1ssu  7435  aptiprleml  7440  mulcomsrg  7558  mulasssrg  7559  distrsrg  7560  aptisr  7580  mulcnsr  7636  cnegex  7933  muladd  8139  lemul12b  8612  qaddcl  9420  iooshf  9728  elfzomelpfzo  10001  expnegzap  10320  setscom  11988  cnpnei  12377