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  7748  addassnqg  7749  nqtri3or  7763  lt2addnq  7771  lt2mulnq  7772  enq0ref  7800  enq0tr  7801  nqnq0pi  7805  nqpnq0nq  7820  nqnq0a  7821  distrnq0  7826  addassnq0lemcl  7828  ltsrprg  8114  mulcomsrg  8124  mulasssrg  8125  distrsrg  8126  aptisr  8146  mulcnsr  8202  cnegex  8505  sub4  8572  muladd  8712  ltleadd  8775  divdivdivap  9045  divadddivap  9059  ltmul12a  9192  fzrev  10501  facndiv  11191  cncongr1  12897  ghmeql  14119  blbas  15583  cncfmet  15742  ptolemy  15975