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  5766  fcof1o  5832  infnfi  6951  addcomnqg  7441  addassnqg  7442  nqtri3or  7456  ltexnqq  7468  nqnq0pi  7498  nqpnq0nq  7513  nqnq0a  7514  addassnq0lemcl  7521  ltaddpr  7657  ltexprlemloc  7667  addcanprlemu  7675  recexprlem1ssu  7694  aptiprleml  7699  mulcomsrg  7817  mulasssrg  7818  distrsrg  7819  aptisr  7839  mulcnsr  7895  cnegex  8197  muladd  8403  lemul12b  8880  qaddcl  9700  iooshf  10018  elfzomelpfzo  10298  expnegzap  10644  setscom  12658  grplmulf1o  13146  lmodfopne  13822  cnpnei  14387  cxplt3  15054  cxple3  15055