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 )

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  5914  fcof1o  5985  infnfi  7189  addcomnqg  7738  addassnqg  7739  nqtri3or  7753  ltexnqq  7765  nqnq0pi  7795  nqpnq0nq  7810  nqnq0a  7811  addassnq0lemcl  7818  ltaddpr  7954  ltexprlemloc  7964  addcanprlemu  7972  recexprlem1ssu  7991  aptiprleml  7996  mulcomsrg  8114  mulasssrg  8115  distrsrg  8116  aptisr  8136  mulcnsr  8192  cnegex  8494  muladd  8701  lemul12b  9181  qaddcl  10014  iooshf  10333  elfzomelpfzo  10627  expnegzap  10988  swrdccatin1  11475  setscom  13370  grplmulf1o  13856  lmodfopne  14635  cnpnei  15243  cxplt3  15945  cxple3  15946  umgr2edg  16362