Theorem 3adantr1 1220

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adantr1

Step	Hyp	Ref	Expression
1		3simpc 1060	. 2 |- ( ( ta /\ ps /\ ch ) -> ( ps /\ ch ) )
2		3adantr.1	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	1, 2	sylan2 491	1 |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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  df-3an 1039

This theorem is referenced by:  3ad2antr3  1228  3adant3r1  1274  swopo  5045  omeulem1  7662  divmuldiv  10725  imasmnd2  17327  imasgrp2  17530  srgbinomlem2  18541  imasring  18619  abvdiv  18837  mdetunilem9  20426  lly1stc  21299  icccvx  22749  dchrpt  24992  dipsubdir  27703  poimirlem4  33413  fdc  33541  unichnidl  33830  dmncan1  33875  pexmidlem6N  35261  erngdvlem3  36278  erngdvlem3-rN  36286  dvalveclem  36314  dvhvaddass  36386  dvhlveclem  36397  issmflem  40936