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  8489  muladd  8712  mulsub  8729  apreim  8933  divmuleqap  9049  ltmul12a  9192  lemul12b  9193  lemul12a  9194  qaddcl  10044  qmulcl  10046  iooshf  10364  fzass4  10478  elfzomelpfzo  10659  swrdccatin2  11515  pfxccatin12  11519  tanaddaplem  12521  issubg4m  14045  ghmpreima  14118  islmodd  14678  opnneissb  15305  neitx  15418  txcnmpt  15423  txrest  15426  metcnp3  15661  cncfmet  15742  dveflem  15876  lgsdir2  16250