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  5737  fiunsnnn  7069  addcomnqg  7600  addassnqg  7601  nqtri3or  7615  lt2addnq  7623  lt2mulnq  7624  enq0ref  7652  enq0tr  7653  nqnq0pi  7657  nqpnq0nq  7672  nqnq0a  7673  distrnq0  7678  addassnq0lemcl  7680  ltsrprg  7966  mulcomsrg  7976  mulasssrg  7977  distrsrg  7978  aptisr  7998  mulcnsr  8054  cnegex  8356  sub4  8423  muladd  8562  ltleadd  8625  divdivdivap  8892  divadddivap  8906  ltmul12a  9039  fzrev  10318  facndiv  11000  cncongr1  12674  ghmeql  13853  blbas  15156  cncfmet  15315  ptolemy  15547