Theorem ad2ant2rl 508

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 475	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantlr 474	1 |- ( ( ( ph /\ th ) /\ ( ta /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  fvtp1g  5704  fcof1o  5768  infnfi  6873  addcomnqg  7343  addassnqg  7344  nqtri3or  7358  ltexnqq  7370  nqnq0pi  7400  nqpnq0nq  7415  nqnq0a  7416  addassnq0lemcl  7423  ltaddpr  7559  ltexprlemloc  7569  addcanprlemu  7577  recexprlem1ssu  7596  aptiprleml  7601  mulcomsrg  7719  mulasssrg  7720  distrsrg  7721  aptisr  7741  mulcnsr  7797  cnegex  8097  muladd  8303  lemul12b  8777  qaddcl  9594  iooshf  9909  elfzomelpfzo  10187  expnegzap  10510  setscom  12456  cnpnei  13013  cxplt3  13634  cxple3  13635