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  8504  muladd  8711  lemul12b  9191  qaddcl  10035  iooshf  10354  elfzomelpfzo  10649  expnegzap  11010  swrdccatin1  11497  setscom  13392  grplmulf1o  13879  lmodfopne  14663  cnpnei  15320  cxplt3  16022  cxple3  16023  umgr2edg  16448