Theorem ad2ant2lr 507

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

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  mpteqb  5586  fiunsnnn  6859  addcomnqg  7343  addassnqg  7344  nqtri3or  7358  lt2addnq  7366  lt2mulnq  7367  enq0ref  7395  enq0tr  7396  nqnq0pi  7400  nqpnq0nq  7415  nqnq0a  7416  distrnq0  7421  addassnq0lemcl  7423  ltsrprg  7709  mulcomsrg  7719  mulasssrg  7720  distrsrg  7721  aptisr  7741  mulcnsr  7797  cnegex  8097  sub4  8164  muladd  8303  ltleadd  8365  divdivdivap  8630  divadddivap  8644  ltmul12a  8776  fzrev  10040  facndiv  10673  cncongr1  12057  blbas  13227  cncfmet  13373  ptolemy  13539