Description: Obsolete version of eqeqan12d as of 23-Oct-2024. (Contributed by NM, 9-Aug-1994) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 20-Nov-2019) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A = B )
|- ( ps -> C = D )
|- ( ( ph /\ ps ) -> ( A = C <-> B = D ) )
|- ( ( ph /\ ps ) -> A = B )
|- ( ( ph /\ ps ) -> C = D )