Theorem ad2ant2l 500

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 470	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantll 468	1 |- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  mpteqb  5519  mpofun  5881  xpdom2  6733  addcmpblnq  7199  addpipqqslem  7201  addpipqqs  7202  addclnq  7207  addcomnqg  7213  addassnqg  7214  mulcomnqg  7215  mulassnqg  7216  distrnqg  7219  ltdcnq  7229  enq0ref  7265  addcmpblnq0  7275  addclnq0  7283  nqpnq0nq  7285  nqnq0a  7286  nqnq0m  7287  distrnq0  7291  mulcomnq0  7292  addassnq0lemcl  7293  genpdisj  7355  appdiv0nq  7396  addcomsrg  7587  mulcomsrg  7589  mulasssrg  7590  distrsrg  7591  addcnsr  7666  mulcnsr  7667  addcnsrec  7674  axaddcl  7696  axmulcl  7698  axaddcom  7702  add42  7948  muladd  8170  mulsub  8187  apreim  8389  divmuleqap  8501  ltmul12a  8642  lemul12b  8643  lemul12a  8644  qaddcl  9454  qmulcl  9456  iooshf  9765  fzass4  9873  elfzomelpfzo  10039  tanaddaplem  11481  opnneissb  12363  neitx  12476  txcnmpt  12481  txrest  12484  metcnp3  12719  cncfmet  12787  dveflem  12895