Theorem ad2ant2l 512

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  mpteqb  5799  mpofun  6193  xpdom2  7135  addcmpblnq  7740  addpipqqslem  7742  addpipqqs  7743  addclnq  7748  addcomnqg  7754  addassnqg  7755  mulcomnqg  7756  mulassnqg  7757  distrnqg  7760  ltdcnq  7770  enq0ref  7806  addcmpblnq0  7816  addclnq0  7824  nqpnq0nq  7826  nqnq0a  7827  nqnq0m  7828  distrnq0  7832  mulcomnq0  7833  addassnq0lemcl  7834  genpdisj  7896  appdiv0nq  7937  addcomsrg  8128  mulcomsrg  8130  mulasssrg  8131  distrsrg  8132  addcnsr  8207  mulcnsr  8208  addcnsrec  8215  axaddcl  8237  axmulcl  8239  axaddcom  8243  add42  8495  muladd  8718  mulsub  8735  apreim  8939  divmuleqap  9055  ltmul12a  9198  lemul12b  9199  lemul12a  9200  qaddcl  10050  qmulcl  10052  iooshf  10370  fzass4  10484  elfzomelpfzo  10665  swrdccatin2  11522  pfxccatin12  11526  tanaddaplem  12529  issubg4m  14054  ghmpreima  14127  cntzsubg  14170  islmodd  14737  opnneissb  15398  neitx  15511  txcnmpt  15516  txrest  15519  metcnp3  15754  cncfmet  15835  dveflem  15969  efnnfsumcl  16256  efchtqdvds  16282  lgsdir2  16374