Theorem adantrrr 761

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
adantrrr	|- ( ( ph /\ ( ps /\ ( ch /\ ta ) ) ) -> th )

Proof of Theorem adantrrr

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ch /\ ta ) -> ch )
2		adantr2.1	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1, 2	sylanr2 685	1 |- ( ( ph /\ ( ps /\ ( ch /\ ta ) ) ) -> 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:  2ndconst  7266  zorn2lem6  9323  addsrmo  9894  mulsrmo  9895  lemul12b  10880  lt2mul2div  10901  lediv12a  10916  tgcl  20773  neissex  20931  alexsublem  21848  alexsubALTlem4  21854  iscmet3  23091  ablo4  27404  shscli  28176  mdslmd3i  29191  cvmliftmolem2  31264  mblfinlem4  33449  heibor  33620  ablo4pnp  33679  crngm4  33802  cvratlem  34707  ps-2  34764  cdlemftr3  35853  mzpcompact2lem  37314