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  5768  mpofun  6155  xpdom2  7082  addcmpblnq  7682  addpipqqslem  7684  addpipqqs  7685  addclnq  7690  addcomnqg  7696  addassnqg  7697  mulcomnqg  7698  mulassnqg  7699  distrnqg  7702  ltdcnq  7712  enq0ref  7748  addcmpblnq0  7758  addclnq0  7766  nqpnq0nq  7768  nqnq0a  7769  nqnq0m  7770  distrnq0  7774  mulcomnq0  7775  addassnq0lemcl  7776  genpdisj  7838  appdiv0nq  7879  addcomsrg  8070  mulcomsrg  8072  mulasssrg  8073  distrsrg  8074  addcnsr  8149  mulcnsr  8150  addcnsrec  8157  axaddcl  8179  axmulcl  8181  axaddcom  8185  add42  8435  muladd  8657  mulsub  8674  apreim  8877  divmuleqap  8991  ltmul12a  9134  lemul12b  9135  lemul12a  9136  qaddcl  9967  qmulcl  9969  iooshf  10285  fzass4  10396  elfzomelpfzo  10576  swrdccatin2  11421  pfxccatin12  11425  tanaddaplem  12424  issubg4m  13910  ghmpreima  13983  islmodd  14441  opnneissb  15020  neitx  15133  txcnmpt  15138  txrest  15141  metcnp3  15376  cncfmet  15457  dveflem  15591  lgsdir2  15906