Metamath Proof Explorer


Theorem wfis3

Description: Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011)

Ref Expression
Hypotheses wfis3.1 RWeA
wfis3.2 RSeA
wfis3.3 y=zφψ
wfis3.4 y=Bφχ
wfis3.5 yAzPredRAyψφ
Assertion wfis3 BAχ

Proof

Step Hyp Ref Expression
1 wfis3.1 RWeA
2 wfis3.2 RSeA
3 wfis3.3 y=zφψ
4 wfis3.4 y=Bφχ
5 wfis3.5 yAzPredRAyψφ
6 1 2 3 5 wfis2 yAφ
7 4 6 vtoclga BAχ