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  5725  mpofun  6106  xpdom2  6990  addcmpblnq  7554  addpipqqslem  7556  addpipqqs  7557  addclnq  7562  addcomnqg  7568  addassnqg  7569  mulcomnqg  7570  mulassnqg  7571  distrnqg  7574  ltdcnq  7584  enq0ref  7620  addcmpblnq0  7630  addclnq0  7638  nqpnq0nq  7640  nqnq0a  7641  nqnq0m  7642  distrnq0  7646  mulcomnq0  7647  addassnq0lemcl  7648  genpdisj  7710  appdiv0nq  7751  addcomsrg  7942  mulcomsrg  7944  mulasssrg  7945  distrsrg  7946  addcnsr  8021  mulcnsr  8022  addcnsrec  8029  axaddcl  8051  axmulcl  8053  axaddcom  8057  add42  8308  muladd  8530  mulsub  8547  apreim  8750  divmuleqap  8864  ltmul12a  9007  lemul12b  9008  lemul12a  9009  qaddcl  9830  qmulcl  9832  iooshf  10148  fzass4  10258  elfzomelpfzo  10437  swrdccatin2  11261  pfxccatin12  11265  tanaddaplem  12249  issubg4m  13730  ghmpreima  13803  islmodd  14257  opnneissb  14829  neitx  14942  txcnmpt  14947  txrest  14950  metcnp3  15185  cncfmet  15266  dveflem  15400  lgsdir2  15712