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  5862  fcof1o  5930  infnfi  7084  addcomnqg  7601  addassnqg  7602  nqtri3or  7616  ltexnqq  7628  nqnq0pi  7658  nqpnq0nq  7673  nqnq0a  7674  addassnq0lemcl  7681  ltaddpr  7817  ltexprlemloc  7827  addcanprlemu  7835  recexprlem1ssu  7854  aptiprleml  7859  mulcomsrg  7977  mulasssrg  7978  distrsrg  7979  aptisr  7999  mulcnsr  8055  cnegex  8357  muladd  8563  lemul12b  9041  qaddcl  9869  iooshf  10187  elfzomelpfzo  10477  expnegzap  10836  swrdccatin1  11310  setscom  13140  grplmulf1o  13675  lmodfopne  14359  cnpnei  14962  cxplt3  15663  cxple3  15664  umgr2edg  16077