Theorem ad2ant2lr 514

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 483	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 480	1 |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  mpteqb  5799  fiunsnnn  7189  addcomnqg  7754  addassnqg  7755  nqtri3or  7769  lt2addnq  7777  lt2mulnq  7778  enq0ref  7806  enq0tr  7807  nqnq0pi  7811  nqpnq0nq  7826  nqnq0a  7827  distrnq0  7832  addassnq0lemcl  7834  ltsrprg  8120  mulcomsrg  8130  mulasssrg  8131  distrsrg  8132  aptisr  8152  mulcnsr  8208  cnegex  8511  sub4  8578  muladd  8718  ltleadd  8781  divdivdivap  9051  divadddivap  9065  ltmul12a  9198  fzrev  10508  facndiv  11199  cncongr1  12906  ghmeql  14129  blbas  15659  cncfmet  15818  ptolemy  16051