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  5796  fiunsnnn  7185  addcomnqg  7749  addassnqg  7750  nqtri3or  7764  lt2addnq  7772  lt2mulnq  7773  enq0ref  7801  enq0tr  7802  nqnq0pi  7806  nqpnq0nq  7821  nqnq0a  7822  distrnq0  7827  addassnq0lemcl  7829  ltsrprg  8115  mulcomsrg  8125  mulasssrg  8126  distrsrg  8127  aptisr  8147  mulcnsr  8203  cnegex  8506  sub4  8573  muladd  8713  ltleadd  8776  divdivdivap  9046  divadddivap  9060  ltmul12a  9193  fzrev  10502  facndiv  11193  cncongr1  12900  ghmeql  14123  blbas  15625  cncfmet  15784  ptolemy  16017