Metamath Proof Explorer

Theorem rdgeq12

Description: Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion rdgeq12 
|- ( ( F = G /\ A = B ) -> rec ( F , A ) = rec ( G , B ) )

Proof

Step Hyp Ref Expression
1 rdgeq2 
 |-  ( A = B -> rec ( F , A ) = rec ( F , B ) )
2 rdgeq1 
 |-  ( F = G -> rec ( F , B ) = rec ( G , B ) )
3 1 2 sylan9eqr 
 |-  ( ( F = G /\ A = B ) -> rec ( F , A ) = rec ( G , B ) )