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  5870  fcof1o  5940  infnfi  7127  addcomnqg  7661  addassnqg  7662  nqtri3or  7676  ltexnqq  7688  nqnq0pi  7718  nqpnq0nq  7733  nqnq0a  7734  addassnq0lemcl  7741  ltaddpr  7877  ltexprlemloc  7887  addcanprlemu  7895  recexprlem1ssu  7914  aptiprleml  7919  mulcomsrg  8037  mulasssrg  8038  distrsrg  8039  aptisr  8059  mulcnsr  8115  cnegex  8416  muladd  8622  lemul12b  9100  qaddcl  9930  iooshf  10248  elfzomelpfzo  10539  expnegzap  10898  swrdccatin1  11372  setscom  13202  grplmulf1o  13737  lmodfopne  14422  cnpnei  15030  cxplt3  15731  cxple3  15732  umgr2edg  16148