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  7749  addassnqg  7750  nqtri3or  7764  ltexnqq  7776  nqnq0pi  7806  nqpnq0nq  7821  nqnq0a  7822  addassnq0lemcl  7829  ltaddpr  7965  ltexprlemloc  7975  addcanprlemu  7983  recexprlem1ssu  8002  aptiprleml  8007  mulcomsrg  8125  mulasssrg  8126  distrsrg  8127  aptisr  8147  mulcnsr  8203  cnegex  8506  muladd  8713  lemul12b  9194  qaddcl  10045  iooshf  10365  elfzomelpfzo  10660  expnegzap  11025  swrdccatin1  11513  setscom  13444  grplmulf1o  13932  lmodfopne  14747  cnpnei  15411  cxplt3  16117  cxple3  16118  umgr2edg  16614