Theorem ad2ant2rl 515

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  fvtp1g  5923  fcof1o  5995  infnfi  7199  addcomnqg  7748  addassnqg  7749  nqtri3or  7763  ltexnqq  7775  nqnq0pi  7805  nqpnq0nq  7820  nqnq0a  7821  addassnq0lemcl  7828  ltaddpr  7964  ltexprlemloc  7974  addcanprlemu  7982  recexprlem1ssu  8001  aptiprleml  8006  mulcomsrg  8124  mulasssrg  8125  distrsrg  8126  aptisr  8146  mulcnsr  8202  cnegex  8505  muladd  8712  lemul12b  9193  qaddcl  10044  iooshf  10364  elfzomelpfzo  10659  expnegzap  11023  swrdccatin1  11511  setscom  13441  grplmulf1o  13928  lmodfopne  14712  cnpnei  15369  cxplt3  16075  cxple3  16076  umgr2edg  16546