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  5773  mpofun  6163  xpdom2  7095  addcmpblnq  7698  addpipqqslem  7700  addpipqqs  7701  addclnq  7706  addcomnqg  7712  addassnqg  7713  mulcomnqg  7714  mulassnqg  7715  distrnqg  7718  ltdcnq  7728  enq0ref  7764  addcmpblnq0  7774  addclnq0  7782  nqpnq0nq  7784  nqnq0a  7785  nqnq0m  7786  distrnq0  7790  mulcomnq0  7791  addassnq0lemcl  7792  genpdisj  7854  appdiv0nq  7895  addcomsrg  8086  mulcomsrg  8088  mulasssrg  8089  distrsrg  8090  addcnsr  8165  mulcnsr  8166  addcnsrec  8173  axaddcl  8195  axmulcl  8197  axaddcom  8201  add42  8451  muladd  8674  mulsub  8691  apreim  8894  divmuleqap  9008  ltmul12a  9151  lemul12b  9152  lemul12a  9153  qaddcl  9985  qmulcl  9987  iooshf  10304  fzass4  10417  elfzomelpfzo  10598  swrdccatin2  11446  pfxccatin12  11450  tanaddaplem  12449  issubg4m  13946  ghmpreima  14019  islmodd  14567  opnneissb  15146  neitx  15259  txcnmpt  15264  txrest  15267  metcnp3  15502  cncfmet  15583  dveflem  15717  lgsdir2  16032