Theorem ad2ant2l 500

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 470	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantll 468	1 |- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  mpteqb  5551  mpofun  5913  xpdom2  6765  addcmpblnq  7266  addpipqqslem  7268  addpipqqs  7269  addclnq  7274  addcomnqg  7280  addassnqg  7281  mulcomnqg  7282  mulassnqg  7283  distrnqg  7286  ltdcnq  7296  enq0ref  7332  addcmpblnq0  7342  addclnq0  7350  nqpnq0nq  7352  nqnq0a  7353  nqnq0m  7354  distrnq0  7358  mulcomnq0  7359  addassnq0lemcl  7360  genpdisj  7422  appdiv0nq  7463  addcomsrg  7654  mulcomsrg  7656  mulasssrg  7657  distrsrg  7658  addcnsr  7733  mulcnsr  7734  addcnsrec  7741  axaddcl  7763  axmulcl  7765  axaddcom  7769  add42  8016  muladd  8238  mulsub  8255  apreim  8457  divmuleqap  8569  ltmul12a  8710  lemul12b  8711  lemul12a  8712  qaddcl  9522  qmulcl  9524  iooshf  9834  fzass4  9942  elfzomelpfzo  10108  tanaddaplem  11612  opnneissb  12494  neitx  12607  txcnmpt  12612  txrest  12615  metcnp3  12850  cncfmet  12918  dveflem  13026