Metamath Proof Explorer


Theorem frpoins3g

Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses frpoins3g.1 x A y Pred R A x ψ φ
frpoins3g.2 x = y φ ψ
frpoins3g.3 x = B φ χ
Assertion frpoins3g R Fr A R Po A R Se A B A χ

Proof

Step Hyp Ref Expression
1 frpoins3g.1 x A y Pred R A x ψ φ
2 frpoins3g.2 x = y φ ψ
3 frpoins3g.3 x = B φ χ
4 1 2 frpoins2g R Fr A R Po A R Se A x A φ
5 3 rspccva x A φ B A χ
6 4 5 sylan R Fr A R Po A R Se A B A χ