Theorem dedths

Description: A version of weak deduction theorem dedth using explicit substitution. (Contributed by NM, 15-Jun-2019)

	Ref	Expression
Hypothesis	dedths.1	|- [. if ( ph , x , B ) / x ]. ps
Assertion	dedths	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		dedths.1	|- [. if ( ph , x , B ) / x ]. ps
2		dfsbcq	|- ( x = if ( [. x / x ]. ph , x , B ) -> ( [. x / x ]. ps <-> [. if ( [. x / x ]. ph , x , B ) / x ]. ps ) )
3		sbcid	|- ( [. x / x ]. ph <-> ph )
4		ifbi	|- ( ( [. x / x ]. ph <-> ph ) -> if ( [. x / x ]. ph , x , B ) = if ( ph , x , B ) )
5		dfsbcq	|- ( if ( [. x / x ]. ph , x , B ) = if ( ph , x , B ) -> ( [. if ( [. x / x ]. ph , x , B ) / x ]. ps <-> [. if ( ph , x , B ) / x ]. ps ) )
6	3 4 5	mp2b	|- ( [. if ( [. x / x ]. ph , x , B ) / x ]. ps <-> [. if ( ph , x , B ) / x ]. ps )
7	1 6	mpbir	|- [. if ( [. x / x ]. ph , x , B ) / x ]. ps
8	2 7	dedth	|- ( [. x / x ]. ph -> [. x / x ]. ps )
9		sbcid	|- ( [. x / x ]. ps <-> ps )
10	8 3 9	3imtr3i	|- ( ph -> ps )