theorem splitb1 (G: wff) (a b c: nat) (p: wff): $ G -> a = b1 c -> p $ > $ G -> b = c -> a = b1 b -> p $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 |
hyp h |
G -> a = b1 c -> p |
|
2 |
G /\ b = c /\ a = b1 b -> G |
||
3 |
G /\ b = c /\ a = b1 b -> a = b1 b |
||
4 |
G /\ b = c /\ a = b1 b -> b = c |
||
5 |
G /\ b = c /\ a = b1 b -> b1 b = b1 c |
||
6 |
G /\ b = c /\ a = b1 b -> a = b1 c |
||
7 |
G /\ b = c /\ a = b1 b -> p |
||
8 |
G /\ b = c -> a = b1 b -> p |
||
9 |
G -> b = c -> a = b1 b -> p |