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  5926  fcof1o  5998  infnfi  7203  addcomnqg  7754  addassnqg  7755  nqtri3or  7769  ltexnqq  7781  nqnq0pi  7811  nqpnq0nq  7826  nqnq0a  7827  addassnq0lemcl  7834  ltaddpr  7970  ltexprlemloc  7980  addcanprlemu  7988  recexprlem1ssu  8007  aptiprleml  8012  mulcomsrg  8130  mulasssrg  8131  distrsrg  8132  aptisr  8152  mulcnsr  8208  cnegex  8511  muladd  8718  lemul12b  9199  qaddcl  10051  iooshf  10371  elfzomelpfzo  10666  expnegzap  11031  swrdccatin1  11519  setscom  13450  grplmulf1o  13938  lmodfopne  14772  cnpnei  15445  cxplt3  16155  cxple3  16156  umgr2edg  16653