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

This proof depends on syntax axioms:  kct 10  ⊧wffMMJ2 11

This proof depends on axioms:  ax-syl 15  ax-jca 17  ax-id 24  ax-cb1 29

This theorem is used by:  hbov  111  hbct  155