Theorem ad2ant2lr 507

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpteqb  5584  fiunsnnn  6855  addcomnqg  7330  addassnqg  7331  nqtri3or  7345  lt2addnq  7353  lt2mulnq  7354  enq0ref  7382  enq0tr  7383  nqnq0pi  7387  nqpnq0nq  7402  nqnq0a  7403  distrnq0  7408  addassnq0lemcl  7410  ltsrprg  7696  mulcomsrg  7706  mulasssrg  7707  distrsrg  7708  aptisr  7728  mulcnsr  7784  cnegex  8084  sub4  8151  muladd  8290  ltleadd  8352  divdivdivap  8617  divadddivap  8631  ltmul12a  8763  fzrev  10027  facndiv  10660  cncongr1  12044  blbas  13148  cncfmet  13294  ptolemy  13460