Theorem ad2ant2lr 479

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

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  mpteqb  5261  fiunsnnn  6338  addcomnqg  6479  addassnqg  6480  nqtri3or  6494  lt2addnq  6502  lt2mulnq  6503  enq0ref  6531  enq0tr  6532  nqnq0pi  6536  nqpnq0nq  6551  nqnq0a  6552  distrnq0  6557  addassnq0lemcl  6559  ltsrprg  6832  mulcomsrg  6842  mulasssrg  6843  distrsrg  6844  aptisr  6863  mulcnsr  6911  cnegex  7189  sub4  7256  muladd  7381  ltleadd  7441  divdivdivap  7689  divadddivap  7703  ltmul12a  7826  fzrev  8946