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  5770  fcof1o  5836  infnfi  6956  addcomnqg  7448  addassnqg  7449  nqtri3or  7463  ltexnqq  7475  nqnq0pi  7505  nqpnq0nq  7520  nqnq0a  7521  addassnq0lemcl  7528  ltaddpr  7664  ltexprlemloc  7674  addcanprlemu  7682  recexprlem1ssu  7701  aptiprleml  7706  mulcomsrg  7824  mulasssrg  7825  distrsrg  7826  aptisr  7846  mulcnsr  7902  cnegex  8204  muladd  8410  lemul12b  8888  qaddcl  9709  iooshf  10027  elfzomelpfzo  10307  expnegzap  10665  setscom  12718  grplmulf1o  13206  lmodfopne  13882  cnpnei  14455  cxplt3  15156  cxple3  15157