Theorem ad2ant2lr 501

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
ad2ant2lr	|- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )

Proof of Theorem ad2ant2lr

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrr 470	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 467	1 |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpteqb  5504  fiunsnnn  6768  addcomnqg  7182  addassnqg  7183  nqtri3or  7197  lt2addnq  7205  lt2mulnq  7206  enq0ref  7234  enq0tr  7235  nqnq0pi  7239  nqpnq0nq  7254  nqnq0a  7255  distrnq0  7260  addassnq0lemcl  7262  ltsrprg  7548  mulcomsrg  7558  mulasssrg  7559  distrsrg  7560  aptisr  7580  mulcnsr  7636  cnegex  7933  sub4  8000  muladd  8139  ltleadd  8201  divdivdivap  8466  divadddivap  8480  ltmul12a  8611  fzrev  9857  facndiv  10478  cncongr1  11773  blbas  12591  cncfmet  12737  ptolemy  12894