Theorem ad2ant2l 508

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
ad2ant2l	|- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrl 478	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantll 476	1 |- ( ( ( th /\ ph ) /\ ( 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:  mpteqb  5619  mpofun  5990  xpdom2  6844  addcmpblnq  7379  addpipqqslem  7381  addpipqqs  7382  addclnq  7387  addcomnqg  7393  addassnqg  7394  mulcomnqg  7395  mulassnqg  7396  distrnqg  7399  ltdcnq  7409  enq0ref  7445  addcmpblnq0  7455  addclnq0  7463  nqpnq0nq  7465  nqnq0a  7466  nqnq0m  7467  distrnq0  7471  mulcomnq0  7472  addassnq0lemcl  7473  genpdisj  7535  appdiv0nq  7576  addcomsrg  7767  mulcomsrg  7769  mulasssrg  7770  distrsrg  7771  addcnsr  7846  mulcnsr  7847  addcnsrec  7854  axaddcl  7876  axmulcl  7878  axaddcom  7882  add42  8132  muladd  8354  mulsub  8371  apreim  8573  divmuleqap  8687  ltmul12a  8830  lemul12b  8831  lemul12a  8832  qaddcl  9648  qmulcl  9650  iooshf  9965  fzass4  10075  elfzomelpfzo  10244  tanaddaplem  11759  issubg4m  13082  islmodd  13446  opnneissb  13895  neitx  14008  txcnmpt  14013  txrest  14016  metcnp3  14251  cncfmet  14319  dveflem  14427  lgsdir2  14674