Theorem mpdan 35

Description: Modus ponens deduction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
mpdan.1	|- R |= S
mpdan.2	|- (R, S) |= T

Assertion

Ref	Expression
mpdan	|- R |= T

Proof of Theorem mpdan

Step	Hyp	Ref	Expression
1		mpdan.1	. . . 4 |- R |= S
2	1	ax-cb1 29	. . 3 |- R:*
3	2	id 25	. 2 |- R |= R
4		mpdan.2	. 2 |- (R, S) |= T
5	3, 1, 4	syl2anc 19	1 |- R |= T

Syntax hints:  kct 10   |= wffMMJ2 11

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-id 24  ax-cb1 29

This theorem is referenced by:  hbov  111  hbct  155