Theorem ad2ant2l 493

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpteqb  5408  mpt2fun  5763  xpdom2  6603  addcmpblnq  6989  addpipqqslem  6991  addpipqqs  6992  addclnq  6997  addcomnqg  7003  addassnqg  7004  mulcomnqg  7005  mulassnqg  7006  distrnqg  7009  ltdcnq  7019  enq0ref  7055  addcmpblnq0  7065  addclnq0  7073  nqpnq0nq  7075  nqnq0a  7076  nqnq0m  7077  distrnq0  7081  mulcomnq0  7082  addassnq0lemcl  7083  genpdisj  7145  appdiv0nq  7186  addcomsrg  7364  mulcomsrg  7366  mulasssrg  7367  distrsrg  7368  addcnsr  7434  mulcnsr  7435  addcnsrec  7442  axaddcl  7464  axmulcl  7466  axaddcom  7468  add42  7707  muladd  7925  mulsub  7942  apreim  8143  divmuleqap  8247  ltmul12a  8384  lemul12b  8385  lemul12a  8386  qaddcl  9183  qmulcl  9185  iooshf  9433  fzass4  9539  elfzomelpfzo  9705  tanaddaplem  11092  opnneissb  11918