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  5693  mpofun  6070  xpdom2  6951  addcmpblnq  7515  addpipqqslem  7517  addpipqqs  7518  addclnq  7523  addcomnqg  7529  addassnqg  7530  mulcomnqg  7531  mulassnqg  7532  distrnqg  7535  ltdcnq  7545  enq0ref  7581  addcmpblnq0  7591  addclnq0  7599  nqpnq0nq  7601  nqnq0a  7602  nqnq0m  7603  distrnq0  7607  mulcomnq0  7608  addassnq0lemcl  7609  genpdisj  7671  appdiv0nq  7712  addcomsrg  7903  mulcomsrg  7905  mulasssrg  7906  distrsrg  7907  addcnsr  7982  mulcnsr  7983  addcnsrec  7990  axaddcl  8012  axmulcl  8014  axaddcom  8018  add42  8269  muladd  8491  mulsub  8508  apreim  8711  divmuleqap  8825  ltmul12a  8968  lemul12b  8969  lemul12a  8970  qaddcl  9791  qmulcl  9793  iooshf  10109  fzass4  10219  elfzomelpfzo  10397  swrdccatin2  11220  pfxccatin12  11224  tanaddaplem  12164  issubg4m  13644  ghmpreima  13717  islmodd  14170  opnneissb  14742  neitx  14855  txcnmpt  14860  txrest  14863  metcnp3  15098  cncfmet  15179  dveflem  15313  lgsdir2  15625