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  5655  fiunsnnn  6951  addcomnqg  7465  addassnqg  7466  nqtri3or  7480  lt2addnq  7488  lt2mulnq  7489  enq0ref  7517  enq0tr  7518  nqnq0pi  7522  nqpnq0nq  7537  nqnq0a  7538  distrnq0  7543  addassnq0lemcl  7545  ltsrprg  7831  mulcomsrg  7841  mulasssrg  7842  distrsrg  7843  aptisr  7863  mulcnsr  7919  cnegex  8221  sub4  8288  muladd  8427  ltleadd  8490  divdivdivap  8757  divadddivap  8771  ltmul12a  8904  fzrev  10176  facndiv  10848  cncongr1  12296  ghmeql  13473  blbas  14753  cncfmet  14912  ptolemy  15144