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  5727  mpofun  6112  xpdom2  6998  addcmpblnq  7565  addpipqqslem  7567  addpipqqs  7568  addclnq  7573  addcomnqg  7579  addassnqg  7580  mulcomnqg  7581  mulassnqg  7582  distrnqg  7585  ltdcnq  7595  enq0ref  7631  addcmpblnq0  7641  addclnq0  7649  nqpnq0nq  7651  nqnq0a  7652  nqnq0m  7653  distrnq0  7657  mulcomnq0  7658  addassnq0lemcl  7659  genpdisj  7721  appdiv0nq  7762  addcomsrg  7953  mulcomsrg  7955  mulasssrg  7956  distrsrg  7957  addcnsr  8032  mulcnsr  8033  addcnsrec  8040  axaddcl  8062  axmulcl  8064  axaddcom  8068  add42  8319  muladd  8541  mulsub  8558  apreim  8761  divmuleqap  8875  ltmul12a  9018  lemul12b  9019  lemul12a  9020  qaddcl  9842  qmulcl  9844  iooshf  10160  fzass4  10270  elfzomelpfzo  10449  swrdccatin2  11277  pfxccatin12  11281  tanaddaplem  12265  issubg4m  13746  ghmpreima  13819  islmodd  14273  opnneissb  14845  neitx  14958  txcnmpt  14963  txrest  14966  metcnp3  15201  cncfmet  15282  dveflem  15416  lgsdir2  15728