Theorem adantrlr 759

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantr2.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
adantrlr	|- ( ( ph /\ ( ( ps /\ ta ) /\ ch ) ) -> th )

Proof of Theorem adantrlr

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ps /\ ta ) -> ps )
2		adantr2.1	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1, 2	sylanr1 684	1 |- ( ( ph /\ ( ( ps /\ ta ) /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  smoord  7462  addsrmo  9894  mulsrmo  9895  lediv12a  10916  nrmmetd  22379  pntrmax  25253  ablo4  27404  mdslmd3i  29191  atom1d  29212  fsumiunle  29575  esumiun  30156  poimirlem28  33437  fdc  33541  incsequz  33544  crngm4  33802  ps-2  34764  aacllem  42547