Theorem 3adant2r 1321

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adant2r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3com12 1269	. . 3 |- ( ( ps /\ ph /\ ch ) -> th )
3	2	3adant1r 1319	. 2 |- ( ( ( ps /\ ta ) /\ ph /\ ch ) -> th )
4	3	3com12 1269	1 |- ( ( ph /\ ( ps /\ ta ) /\ 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:  ltdiv23  10914  lediv23  10915  divalglem8  15123  isdrngd  18772  deg1tm  23878  ax5seglem1  25808  ax5seglem2  25809  nvaddsub4  27512  nmoub2i  27629  cdleme21at  35616  cdleme42f  35768  trlcoabs2N  36010  tendoplcl2  36066  tendopltp  36068  cdlemk2  36120  cdlemk8  36126  cdlemk9  36127  cdlemk9bN  36128  cdleml8  36271  dihglblem3N  36584  dihglblem3aN  36585  fourierdlem42  40366  lincscm  42219