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  5716  fcof1o  5780  infnfi  6885  addcomnqg  7355  addassnqg  7356  nqtri3or  7370  ltexnqq  7382  nqnq0pi  7412  nqpnq0nq  7427  nqnq0a  7428  addassnq0lemcl  7435  ltaddpr  7571  ltexprlemloc  7581  addcanprlemu  7589  recexprlem1ssu  7608  aptiprleml  7613  mulcomsrg  7731  mulasssrg  7732  distrsrg  7733  aptisr  7753  mulcnsr  7809  cnegex  8109  muladd  8315  lemul12b  8789  qaddcl  9606  iooshf  9921  elfzomelpfzo  10199  expnegzap  10522  setscom  12467  grplmulf1o  12803  cnpnei  13288  cxplt3  13909  cxple3  13910