Theorem ad2ant2lr 494

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

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  mpteqb  5393  fiunsnnn  6595  addcomnqg  6938  addassnqg  6939  nqtri3or  6953  lt2addnq  6961  lt2mulnq  6962  enq0ref  6990  enq0tr  6991  nqnq0pi  6995  nqpnq0nq  7010  nqnq0a  7011  distrnq0  7016  addassnq0lemcl  7018  ltsrprg  7291  mulcomsrg  7301  mulasssrg  7302  distrsrg  7303  aptisr  7322  mulcnsr  7370  cnegex  7658  sub4  7725  muladd  7860  ltleadd  7922  divdivdivap  8178  divadddivap  8192  ltmul12a  8319  fzrev  9494  facndiv  10143  cncongr1  11359