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  7133  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  10051  qmulcl  10053  iooshf  10371  fzass4  10485  elfzomelpfzo  10666  swrdccatin2  11523  pfxccatin12  11527  tanaddaplem  12530  issubg4m  14055  ghmpreima  14128  cntzsubg  14171  islmodd  14738  opnneissb  15381  neitx  15494  txcnmpt  15499  txrest  15502  metcnp3  15737  cncfmet  15818  dveflem  15952  efnnfsumcl  16239  efchtqdvds  16265  lgsdir2  16357