Theorem ad2ant2l 492

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  mpteqb  5293  mpt2fun  5634  xpdom2  6375  addcmpblnq  6619  addpipqqslem  6621  addpipqqs  6622  addclnq  6627  addcomnqg  6633  addassnqg  6634  mulcomnqg  6635  mulassnqg  6636  distrnqg  6639  ltdcnq  6649  enq0ref  6685  addcmpblnq0  6695  addclnq0  6703  nqpnq0nq  6705  nqnq0a  6706  nqnq0m  6707  distrnq0  6711  mulcomnq0  6712  addassnq0lemcl  6713  genpdisj  6775  appdiv0nq  6816  addcomsrg  6994  mulcomsrg  6996  mulasssrg  6997  distrsrg  6998  addcnsr  7064  mulcnsr  7065  addcnsrec  7072  axaddcl  7094  axmulcl  7096  axaddcom  7098  add42  7337  muladd  7555  mulsub  7572  apreim  7770  divmuleqap  7872  ltmul12a  8005  lemul12b  8006  lemul12a  8007  qaddcl  8801  qmulcl  8803  iooshf  9051  fzass4  9156  elfzomelpfzo  9317