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  5649  mpofun  6021  xpdom2  6887  addcmpblnq  7429  addpipqqslem  7431  addpipqqs  7432  addclnq  7437  addcomnqg  7443  addassnqg  7444  mulcomnqg  7445  mulassnqg  7446  distrnqg  7449  ltdcnq  7459  enq0ref  7495  addcmpblnq0  7505  addclnq0  7513  nqpnq0nq  7515  nqnq0a  7516  nqnq0m  7517  distrnq0  7521  mulcomnq0  7522  addassnq0lemcl  7523  genpdisj  7585  appdiv0nq  7626  addcomsrg  7817  mulcomsrg  7819  mulasssrg  7820  distrsrg  7821  addcnsr  7896  mulcnsr  7897  addcnsrec  7904  axaddcl  7926  axmulcl  7928  axaddcom  7932  add42  8183  muladd  8405  mulsub  8422  apreim  8624  divmuleqap  8738  ltmul12a  8881  lemul12b  8882  lemul12a  8883  qaddcl  9703  qmulcl  9705  iooshf  10021  fzass4  10131  elfzomelpfzo  10301  tanaddaplem  11884  issubg4m  13266  ghmpreima  13339  islmodd  13792  opnneissb  14334  neitx  14447  txcnmpt  14452  txrest  14455  metcnp3  14690  cncfmet  14771  dveflem  14905  lgsdir2  15190