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  5726  fcof1o  5792  infnfi  6897  addcomnqg  7382  addassnqg  7383  nqtri3or  7397  ltexnqq  7409  nqnq0pi  7439  nqpnq0nq  7454  nqnq0a  7455  addassnq0lemcl  7462  ltaddpr  7598  ltexprlemloc  7608  addcanprlemu  7616  recexprlem1ssu  7635  aptiprleml  7640  mulcomsrg  7758  mulasssrg  7759  distrsrg  7760  aptisr  7780  mulcnsr  7836  cnegex  8137  muladd  8343  lemul12b  8820  qaddcl  9637  iooshf  9954  elfzomelpfzo  10233  expnegzap  10556  setscom  12504  grplmulf1o  12949  lmodfopne  13421  cnpnei  13804  cxplt3  14425  cxple3  14426