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  5652  mpofun  6024  xpdom2  6890  addcmpblnq  7434  addpipqqslem  7436  addpipqqs  7437  addclnq  7442  addcomnqg  7448  addassnqg  7449  mulcomnqg  7450  mulassnqg  7451  distrnqg  7454  ltdcnq  7464  enq0ref  7500  addcmpblnq0  7510  addclnq0  7518  nqpnq0nq  7520  nqnq0a  7521  nqnq0m  7522  distrnq0  7526  mulcomnq0  7527  addassnq0lemcl  7528  genpdisj  7590  appdiv0nq  7631  addcomsrg  7822  mulcomsrg  7824  mulasssrg  7825  distrsrg  7826  addcnsr  7901  mulcnsr  7902  addcnsrec  7909  axaddcl  7931  axmulcl  7933  axaddcom  7937  add42  8188  muladd  8410  mulsub  8427  apreim  8630  divmuleqap  8744  ltmul12a  8887  lemul12b  8888  lemul12a  8889  qaddcl  9709  qmulcl  9711  iooshf  10027  fzass4  10137  elfzomelpfzo  10307  tanaddaplem  11903  issubg4m  13323  ghmpreima  13396  islmodd  13849  opnneissb  14391  neitx  14504  txcnmpt  14509  txrest  14512  metcnp3  14747  cncfmet  14828  dveflem  14962  lgsdir2  15274