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  5724  fiunsnnn  7039  addcomnqg  7564  addassnqg  7565  nqtri3or  7579  lt2addnq  7587  lt2mulnq  7588  enq0ref  7616  enq0tr  7617  nqnq0pi  7621  nqpnq0nq  7636  nqnq0a  7637  distrnq0  7642  addassnq0lemcl  7644  ltsrprg  7930  mulcomsrg  7940  mulasssrg  7941  distrsrg  7942  aptisr  7962  mulcnsr  8018  cnegex  8320  sub4  8387  muladd  8526  ltleadd  8589  divdivdivap  8856  divadddivap  8870  ltmul12a  9003  fzrev  10276  facndiv  10956  cncongr1  12620  ghmeql  13799  blbas  15101  cncfmet  15260  ptolemy  15492