Theorem ad2ant2l 512

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 482	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantll 480	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  5790  mpofun  6180  xpdom2  7119  addcmpblnq  7724  addpipqqslem  7726  addpipqqs  7727  addclnq  7732  addcomnqg  7738  addassnqg  7739  mulcomnqg  7740  mulassnqg  7741  distrnqg  7744  ltdcnq  7754  enq0ref  7790  addcmpblnq0  7800  addclnq0  7808  nqpnq0nq  7810  nqnq0a  7811  nqnq0m  7812  distrnq0  7816  mulcomnq0  7817  addassnq0lemcl  7818  genpdisj  7880  appdiv0nq  7921  addcomsrg  8112  mulcomsrg  8114  mulasssrg  8115  distrsrg  8116  addcnsr  8191  mulcnsr  8192  addcnsrec  8199  axaddcl  8221  axmulcl  8223  axaddcom  8227  add42  8478  muladd  8701  mulsub  8718  apreim  8921  divmuleqap  9037  ltmul12a  9180  lemul12b  9181  lemul12a  9182  qaddcl  10014  qmulcl  10016  iooshf  10333  fzass4  10446  elfzomelpfzo  10627  swrdccatin2  11479  pfxccatin12  11483  tanaddaplem  12483  issubg4m  13973  ghmpreima  14046  islmodd  14602  opnneissb  15179  neitx  15292  txcnmpt  15297  txrest  15300  metcnp3  15535  cncfmet  15616  dveflem  15750  lgsdir2  16066