Theorem ad2ant2lr 514

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 483	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 480	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  5790  fiunsnnn  7175  addcomnqg  7738  addassnqg  7739  nqtri3or  7753  lt2addnq  7761  lt2mulnq  7762  enq0ref  7790  enq0tr  7791  nqnq0pi  7795  nqpnq0nq  7810  nqnq0a  7811  distrnq0  7816  addassnq0lemcl  7818  ltsrprg  8104  mulcomsrg  8114  mulasssrg  8115  distrsrg  8116  aptisr  8136  mulcnsr  8192  cnegex  8494  sub4  8561  muladd  8701  ltleadd  8764  divdivdivap  9033  divadddivap  9047  ltmul12a  9180  fzrev  10469  facndiv  11155  cncongr1  12859  ghmeql  14047  blbas  15457  cncfmet  15616  ptolemy  15848