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  5609  fiunsnnn  6884  addcomnqg  7383  addassnqg  7384  nqtri3or  7398  lt2addnq  7406  lt2mulnq  7407  enq0ref  7435  enq0tr  7436  nqnq0pi  7440  nqpnq0nq  7455  nqnq0a  7456  distrnq0  7461  addassnq0lemcl  7463  ltsrprg  7749  mulcomsrg  7759  mulasssrg  7760  distrsrg  7761  aptisr  7781  mulcnsr  7837  cnegex  8138  sub4  8205  muladd  8344  ltleadd  8406  divdivdivap  8673  divadddivap  8687  ltmul12a  8820  fzrev  10087  facndiv  10722  cncongr1  12106  blbas  14073  cncfmet  14219  ptolemy  14385