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  5727  mpofun  6112  xpdom2  6998  addcmpblnq  7562  addpipqqslem  7564  addpipqqs  7565  addclnq  7570  addcomnqg  7576  addassnqg  7577  mulcomnqg  7578  mulassnqg  7579  distrnqg  7582  ltdcnq  7592  enq0ref  7628  addcmpblnq0  7638  addclnq0  7646  nqpnq0nq  7648  nqnq0a  7649  nqnq0m  7650  distrnq0  7654  mulcomnq0  7655  addassnq0lemcl  7656  genpdisj  7718  appdiv0nq  7759  addcomsrg  7950  mulcomsrg  7952  mulasssrg  7953  distrsrg  7954  addcnsr  8029  mulcnsr  8030  addcnsrec  8037  axaddcl  8059  axmulcl  8061  axaddcom  8065  add42  8316  muladd  8538  mulsub  8555  apreim  8758  divmuleqap  8872  ltmul12a  9015  lemul12b  9016  lemul12a  9017  qaddcl  9838  qmulcl  9840  iooshf  10156  fzass4  10266  elfzomelpfzo  10445  swrdccatin2  11269  pfxccatin12  11273  tanaddaplem  12257  issubg4m  13738  ghmpreima  13811  islmodd  14265  opnneissb  14837  neitx  14950  txcnmpt  14955  txrest  14958  metcnp3  15193  cncfmet  15274  dveflem  15408  lgsdir2  15720