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  5576  mpofun  5944  xpdom2  6797  addcmpblnq  7308  addpipqqslem  7310  addpipqqs  7311  addclnq  7316  addcomnqg  7322  addassnqg  7323  mulcomnqg  7324  mulassnqg  7325  distrnqg  7328  ltdcnq  7338  enq0ref  7374  addcmpblnq0  7384  addclnq0  7392  nqpnq0nq  7394  nqnq0a  7395  nqnq0m  7396  distrnq0  7400  mulcomnq0  7401  addassnq0lemcl  7402  genpdisj  7464  appdiv0nq  7505  addcomsrg  7696  mulcomsrg  7698  mulasssrg  7699  distrsrg  7700  addcnsr  7775  mulcnsr  7776  addcnsrec  7783  axaddcl  7805  axmulcl  7807  axaddcom  7811  add42  8060  muladd  8282  mulsub  8299  apreim  8501  divmuleqap  8613  ltmul12a  8755  lemul12b  8756  lemul12a  8757  qaddcl  9573  qmulcl  9575  iooshf  9888  fzass4  9997  elfzomelpfzo  10166  tanaddaplem  11679  opnneissb  12805  neitx  12918  txcnmpt  12923  txrest  12926  metcnp3  13161  cncfmet  13229  dveflem  13337  lgsdir2  13584