Theorem ad2ant2lr 510

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mpteqb  5693  fiunsnnn  7004  addcomnqg  7529  addassnqg  7530  nqtri3or  7544  lt2addnq  7552  lt2mulnq  7553  enq0ref  7581  enq0tr  7582  nqnq0pi  7586  nqpnq0nq  7601  nqnq0a  7602  distrnq0  7607  addassnq0lemcl  7609  ltsrprg  7895  mulcomsrg  7905  mulasssrg  7906  distrsrg  7907  aptisr  7927  mulcnsr  7983  cnegex  8285  sub4  8352  muladd  8491  ltleadd  8554  divdivdivap  8821  divadddivap  8835  ltmul12a  8968  fzrev  10241  facndiv  10921  cncongr1  12540  ghmeql  13718  blbas  15020  cncfmet  15179  ptolemy  15411