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  5773  fiunsnnn  7151  addcomnqg  7712  addassnqg  7713  nqtri3or  7727  lt2addnq  7735  lt2mulnq  7736  enq0ref  7764  enq0tr  7765  nqnq0pi  7769  nqpnq0nq  7784  nqnq0a  7785  distrnq0  7790  addassnq0lemcl  7792  ltsrprg  8078  mulcomsrg  8088  mulasssrg  8089  distrsrg  8090  aptisr  8110  mulcnsr  8166  cnegex  8467  sub4  8534  muladd  8674  ltleadd  8737  divdivdivap  9004  divadddivap  9018  ltmul12a  9151  fzrev  10440  facndiv  11126  cncongr1  12825  ghmeql  14020  blbas  15424  cncfmet  15583  ptolemy  15815