Theorem eqeq12 1487

Description: Equality relationship among 4 classes.

Assertion

Ref	Expression
eqeq12	|- ((A = B /\ C = D) -> (A = C <-> B = D))

Proof of Theorem eqeq12

Step	Hyp	Ref	Expression
1		eqeq1 1481	. 2 |- (A = B -> (A = C <-> B = C))
2		eqeq2 1484	. 2 |- (C = D -> (B = C <-> B = D))
3	1, 2	sylan9bb 540	1 |- ((A = B /\ C = D) -> (A = C <-> B = D))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956

This theorem is referenced by:  funopg 3547  eqfnfv 3797  tfrlem1 3911  tfrlem2 3912  tfr3 3926  th3qlem1 4314  xpdom2 4442  aceq5lem4 4738  kmlem9 4773  zorn2lem6 4793  uzindOLD 6208  xpnnen 7499  grplactf1o 8098  mulid 8132  pslem 8647  hilid 9028  uninqs 10441  eqidob 10723

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain