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  5648  fiunsnnn  6937  addcomnqg  7441  addassnqg  7442  nqtri3or  7456  lt2addnq  7464  lt2mulnq  7465  enq0ref  7493  enq0tr  7494  nqnq0pi  7498  nqpnq0nq  7513  nqnq0a  7514  distrnq0  7519  addassnq0lemcl  7521  ltsrprg  7807  mulcomsrg  7817  mulasssrg  7818  distrsrg  7819  aptisr  7839  mulcnsr  7895  cnegex  8197  sub4  8264  muladd  8403  ltleadd  8465  divdivdivap  8732  divadddivap  8746  ltmul12a  8879  fzrev  10150  facndiv  10810  cncongr1  12241  ghmeql  13337  blbas  14601  cncfmet  14747  ptolemy  14959