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  5653  fiunsnnn  6944  addcomnqg  7451  addassnqg  7452  nqtri3or  7466  lt2addnq  7474  lt2mulnq  7475  enq0ref  7503  enq0tr  7504  nqnq0pi  7508  nqpnq0nq  7523  nqnq0a  7524  distrnq0  7529  addassnq0lemcl  7531  ltsrprg  7817  mulcomsrg  7827  mulasssrg  7828  distrsrg  7829  aptisr  7849  mulcnsr  7905  cnegex  8207  sub4  8274  muladd  8413  ltleadd  8476  divdivdivap  8743  divadddivap  8757  ltmul12a  8890  fzrev  10162  facndiv  10834  cncongr1  12282  ghmeql  13423  blbas  14695  cncfmet  14854  ptolemy  15086