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  5737  fiunsnnn  7070  addcomnqg  7601  addassnqg  7602  nqtri3or  7616  lt2addnq  7624  lt2mulnq  7625  enq0ref  7653  enq0tr  7654  nqnq0pi  7658  nqpnq0nq  7673  nqnq0a  7674  distrnq0  7679  addassnq0lemcl  7681  ltsrprg  7967  mulcomsrg  7977  mulasssrg  7978  distrsrg  7979  aptisr  7999  mulcnsr  8055  cnegex  8357  sub4  8424  muladd  8563  ltleadd  8626  divdivdivap  8893  divadddivap  8907  ltmul12a  9040  fzrev  10319  facndiv  11002  cncongr1  12693  ghmeql  13872  blbas  15176  cncfmet  15335  ptolemy  15567