Metamath Proof Explorer


Theorem frege107

Description: Proposition 107 of Frege1879 p. 74. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege107.v V A
Assertion frege107 Z t+ R I Y Y R V Z t+ R V Z t+ R I Y Y R V Z t+ R I V

Proof

Step Hyp Ref Expression
1 frege107.v V A
2 1 frege106 Z t+ R V Z t+ R I V
3 frege7 Z t+ R V Z t+ R I V Z t+ R I Y Y R V Z t+ R V Z t+ R I Y Y R V Z t+ R I V
4 2 3 ax-mp Z t+ R I Y Y R V Z t+ R V Z t+ R I Y Y R V Z t+ R I V