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 )

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:  mpteqb  5796  mpofun  6190  xpdom2  7129  addcmpblnq  7734  addpipqqslem  7736  addpipqqs  7737  addclnq  7742  addcomnqg  7748  addassnqg  7749  mulcomnqg  7750  mulassnqg  7751  distrnqg  7754  ltdcnq  7764  enq0ref  7800  addcmpblnq0  7810  addclnq0  7818  nqpnq0nq  7820  nqnq0a  7821  nqnq0m  7822  distrnq0  7826  mulcomnq0  7827  addassnq0lemcl  7828  genpdisj  7890  appdiv0nq  7931  addcomsrg  8122  mulcomsrg  8124  mulasssrg  8125  distrsrg  8126  addcnsr  8201  mulcnsr  8202  addcnsrec  8209  axaddcl  8231  axmulcl  8233  axaddcom  8237  add42  8488  muladd  8711  mulsub  8728  apreim  8931  divmuleqap  9047  ltmul12a  9190  lemul12b  9191  lemul12a  9192  qaddcl  10035  qmulcl  10037  iooshf  10354  fzass4  10468  elfzomelpfzo  10649  swrdccatin2  11501  pfxccatin12  11505  tanaddaplem  12505  issubg4m  13996  ghmpreima  14069  islmodd  14629  opnneissb  15256  neitx  15369  txcnmpt  15374  txrest  15377  metcnp3  15612  cncfmet  15693  dveflem  15827  lgsdir2  16152