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  5746  mpofun  6133  xpdom2  7058  addcmpblnq  7647  addpipqqslem  7649  addpipqqs  7650  addclnq  7655  addcomnqg  7661  addassnqg  7662  mulcomnqg  7663  mulassnqg  7664  distrnqg  7667  ltdcnq  7677  enq0ref  7713  addcmpblnq0  7723  addclnq0  7731  nqpnq0nq  7733  nqnq0a  7734  nqnq0m  7735  distrnq0  7739  mulcomnq0  7740  addassnq0lemcl  7741  genpdisj  7803  appdiv0nq  7844  addcomsrg  8035  mulcomsrg  8037  mulasssrg  8038  distrsrg  8039  addcnsr  8114  mulcnsr  8115  addcnsrec  8122  axaddcl  8144  axmulcl  8146  axaddcom  8150  add42  8400  muladd  8622  mulsub  8639  apreim  8842  divmuleqap  8956  ltmul12a  9099  lemul12b  9100  lemul12a  9101  qaddcl  9930  qmulcl  9932  iooshf  10248  fzass4  10359  elfzomelpfzo  10539  swrdccatin2  11376  pfxccatin12  11380  tanaddaplem  12379  issubg4m  13860  ghmpreima  13933  islmodd  14389  opnneissb  14966  neitx  15079  txcnmpt  15084  txrest  15087  metcnp3  15322  cncfmet  15403  dveflem  15537  lgsdir2  15852