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  5608  fiunsnnn  6883  addcomnqg  7382  addassnqg  7383  nqtri3or  7397  lt2addnq  7405  lt2mulnq  7406  enq0ref  7434  enq0tr  7435  nqnq0pi  7439  nqpnq0nq  7454  nqnq0a  7455  distrnq0  7460  addassnq0lemcl  7462  ltsrprg  7748  mulcomsrg  7758  mulasssrg  7759  distrsrg  7760  aptisr  7780  mulcnsr  7836  cnegex  8137  sub4  8204  muladd  8343  ltleadd  8405  divdivdivap  8672  divadddivap  8686  ltmul12a  8819  fzrev  10086  facndiv  10721  cncongr1  12105  blbas  14018  cncfmet  14164  ptolemy  14330