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  8504  sub4  8571  muladd  8711  ltleadd  8774  divdivdivap  9043  divadddivap  9057  ltmul12a  9190  fzrev  10491  facndiv  11177  cncongr1  12881  ghmeql  14070  blbas  15534  cncfmet  15693  ptolemy  15925