Theorem ad2ant2lr 510

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 479	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 476	1 |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> 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  5733  fiunsnnn  7063  addcomnqg  7591  addassnqg  7592  nqtri3or  7606  lt2addnq  7614  lt2mulnq  7615  enq0ref  7643  enq0tr  7644  nqnq0pi  7648  nqpnq0nq  7663  nqnq0a  7664  distrnq0  7669  addassnq0lemcl  7671  ltsrprg  7957  mulcomsrg  7967  mulasssrg  7968  distrsrg  7969  aptisr  7989  mulcnsr  8045  cnegex  8347  sub4  8414  muladd  8553  ltleadd  8616  divdivdivap  8883  divadddivap  8897  ltmul12a  9030  fzrev  10309  facndiv  10991  cncongr1  12665  ghmeql  13844  blbas  15147  cncfmet  15306  ptolemy  15538