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  5740  fiunsnnn  7075  addcomnqg  7606  addassnqg  7607  nqtri3or  7621  lt2addnq  7629  lt2mulnq  7630  enq0ref  7658  enq0tr  7659  nqnq0pi  7663  nqpnq0nq  7678  nqnq0a  7679  distrnq0  7684  addassnq0lemcl  7686  ltsrprg  7972  mulcomsrg  7982  mulasssrg  7983  distrsrg  7984  aptisr  8004  mulcnsr  8060  cnegex  8362  sub4  8429  muladd  8568  ltleadd  8631  divdivdivap  8898  divadddivap  8912  ltmul12a  9045  fzrev  10324  facndiv  11007  cncongr1  12698  ghmeql  13877  blbas  15186  cncfmet  15345  ptolemy  15577