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  5622  mpofun  5993  xpdom2  6849  addcmpblnq  7384  addpipqqslem  7386  addpipqqs  7387  addclnq  7392  addcomnqg  7398  addassnqg  7399  mulcomnqg  7400  mulassnqg  7401  distrnqg  7404  ltdcnq  7414  enq0ref  7450  addcmpblnq0  7460  addclnq0  7468  nqpnq0nq  7470  nqnq0a  7471  nqnq0m  7472  distrnq0  7476  mulcomnq0  7477  addassnq0lemcl  7478  genpdisj  7540  appdiv0nq  7581  addcomsrg  7772  mulcomsrg  7774  mulasssrg  7775  distrsrg  7776  addcnsr  7851  mulcnsr  7852  addcnsrec  7859  axaddcl  7881  axmulcl  7883  axaddcom  7887  add42  8137  muladd  8359  mulsub  8376  apreim  8578  divmuleqap  8692  ltmul12a  8835  lemul12b  8836  lemul12a  8837  qaddcl  9653  qmulcl  9655  iooshf  9970  fzass4  10080  elfzomelpfzo  10249  tanaddaplem  11764  issubg4m  13098  ghmpreima  13166  islmodd  13570  opnneissb  14052  neitx  14165  txcnmpt  14170  txrest  14173  metcnp3  14408  cncfmet  14476  dveflem  14584  lgsdir2  14831