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  5672  mpofun  6049  xpdom2  6928  addcmpblnq  7482  addpipqqslem  7484  addpipqqs  7485  addclnq  7490  addcomnqg  7496  addassnqg  7497  mulcomnqg  7498  mulassnqg  7499  distrnqg  7502  ltdcnq  7512  enq0ref  7548  addcmpblnq0  7558  addclnq0  7566  nqpnq0nq  7568  nqnq0a  7569  nqnq0m  7570  distrnq0  7574  mulcomnq0  7575  addassnq0lemcl  7576  genpdisj  7638  appdiv0nq  7679  addcomsrg  7870  mulcomsrg  7872  mulasssrg  7873  distrsrg  7874  addcnsr  7949  mulcnsr  7950  addcnsrec  7957  axaddcl  7979  axmulcl  7981  axaddcom  7985  add42  8236  muladd  8458  mulsub  8475  apreim  8678  divmuleqap  8792  ltmul12a  8935  lemul12b  8936  lemul12a  8937  qaddcl  9758  qmulcl  9760  iooshf  10076  fzass4  10186  elfzomelpfzo  10362  tanaddaplem  12082  issubg4m  13562  ghmpreima  13635  islmodd  14088  opnneissb  14660  neitx  14773  txcnmpt  14778  txrest  14781  metcnp3  15016  cncfmet  15097  dveflem  15231  lgsdir2  15543