Metamath Proof Explorer


Theorem mthmb

Description: If two statements have the same reduct then one is a theorem iff the other is. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mthmb.r 𝑅 = ( mStRed ‘ 𝑇 )
mthmb.u 𝑈 = ( mThm ‘ 𝑇 )
Assertion mthmb ( ( 𝑅𝑋 ) = ( 𝑅𝑌 ) → ( 𝑋𝑈𝑌𝑈 ) )

Proof

Step Hyp Ref Expression
1 mthmb.r 𝑅 = ( mStRed ‘ 𝑇 )
2 mthmb.u 𝑈 = ( mThm ‘ 𝑇 )
3 1 2 mthmblem ( ( 𝑅𝑋 ) = ( 𝑅𝑌 ) → ( 𝑋𝑈𝑌𝑈 ) )
4 1 2 mthmblem ( ( 𝑅𝑌 ) = ( 𝑅𝑋 ) → ( 𝑌𝑈𝑋𝑈 ) )
5 4 eqcoms ( ( 𝑅𝑋 ) = ( 𝑅𝑌 ) → ( 𝑌𝑈𝑋𝑈 ) )
6 3 5 impbid ( ( 𝑅𝑋 ) = ( 𝑅𝑌 ) → ( 𝑋𝑈𝑌𝑈 ) )