Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frpoins3g.1 | ||
frpoins3g.2 | |||
frpoins3g.3 | |||
Assertion | frpoins3g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frpoins3g.1 | ||
2 | frpoins3g.2 | ||
3 | frpoins3g.3 | ||
4 | 1 2 | frpoins2g | |
5 | 3 | rspccva | |
6 | 4 5 | sylan |