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  5773  fcof1o  5839  infnfi  6965  addcomnqg  7465  addassnqg  7466  nqtri3or  7480  ltexnqq  7492  nqnq0pi  7522  nqpnq0nq  7537  nqnq0a  7538  addassnq0lemcl  7545  ltaddpr  7681  ltexprlemloc  7691  addcanprlemu  7699  recexprlem1ssu  7718  aptiprleml  7723  mulcomsrg  7841  mulasssrg  7842  distrsrg  7843  aptisr  7863  mulcnsr  7919  cnegex  8221  muladd  8427  lemul12b  8905  qaddcl  9726  iooshf  10044  elfzomelpfzo  10324  expnegzap  10682  setscom  12743  grplmulf1o  13276  lmodfopne  13958  cnpnei  14539  cxplt3  15240  cxple3  15241