Metamath Proof Explorer


Theorem frege88

Description: Commuted form of frege87 . Proposition 88 of Frege1879 p. 67. (Contributed by RP, 1-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege87.x X U
frege87.y Y V
frege87.z Z W
frege87.r R S
frege87.a A B
Assertion frege88 Y R Z X t+ R Y w X R w w A R hereditary A Z A

Proof

Step Hyp Ref Expression
1 frege87.x X U
2 frege87.y Y V
3 frege87.z Z W
4 frege87.r R S
5 frege87.a A B
6 1 2 3 4 5 frege87 X t+ R Y w X R w w A R hereditary A Y R Z Z A
7 frege15 X t+ R Y w X R w w A R hereditary A Y R Z Z A Y R Z X t+ R Y w X R w w A R hereditary A Z A
8 6 7 ax-mp Y R Z X t+ R Y w X R w w A R hereditary A Z A