Theorem ad2ant2lr 502

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 471	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 468	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  5576  fiunsnnn  6847  addcomnqg  7322  addassnqg  7323  nqtri3or  7337  lt2addnq  7345  lt2mulnq  7346  enq0ref  7374  enq0tr  7375  nqnq0pi  7379  nqpnq0nq  7394  nqnq0a  7395  distrnq0  7400  addassnq0lemcl  7402  ltsrprg  7688  mulcomsrg  7698  mulasssrg  7699  distrsrg  7700  aptisr  7720  mulcnsr  7776  cnegex  8076  sub4  8143  muladd  8282  ltleadd  8344  divdivdivap  8609  divadddivap  8623  ltmul12a  8755  fzrev  10019  facndiv  10652  cncongr1  12035  blbas  13083  cncfmet  13229  ptolemy  13395