Theorem ad2ant2l 505

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 475	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantll 473	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  5586  mpofun  5955  xpdom2  6809  addcmpblnq  7329  addpipqqslem  7331  addpipqqs  7332  addclnq  7337  addcomnqg  7343  addassnqg  7344  mulcomnqg  7345  mulassnqg  7346  distrnqg  7349  ltdcnq  7359  enq0ref  7395  addcmpblnq0  7405  addclnq0  7413  nqpnq0nq  7415  nqnq0a  7416  nqnq0m  7417  distrnq0  7421  mulcomnq0  7422  addassnq0lemcl  7423  genpdisj  7485  appdiv0nq  7526  addcomsrg  7717  mulcomsrg  7719  mulasssrg  7720  distrsrg  7721  addcnsr  7796  mulcnsr  7797  addcnsrec  7804  axaddcl  7826  axmulcl  7828  axaddcom  7832  add42  8081  muladd  8303  mulsub  8320  apreim  8522  divmuleqap  8634  ltmul12a  8776  lemul12b  8777  lemul12a  8778  qaddcl  9594  qmulcl  9596  iooshf  9909  fzass4  10018  elfzomelpfzo  10187  tanaddaplem  11701  opnneissb  12949  neitx  13062  txcnmpt  13067  txrest  13070  metcnp3  13305  cncfmet  13373  dveflem  13481  lgsdir2  13728