Theorem eqeq12 1484

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 1478	. 2 |- (A = B -> (A = C <-> B = C))
2		eqeq2 1481	. 2 |- (C = D -> (B = C <-> B = D))
3	1, 2	sylan9bb 539	1 |- ((A = B /\ C = D) -> (A = C <-> B = D))

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

This theorem is referenced by:  funopg 3539  eqfnfv 3788  tfrlem1 3902  tfrlem2 3903  tfr3 3917  th3qlem1 4304  xpdom2 4428  aceq5lem4 4718  kmlem9 4753  zorn2lem6 4773  uzindOLD 6164  xpnnen 7449  grplactf1o 8049  mulid 8084  pslem 8590  hilid 8967  uninqs 10378  eqidob 10603

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

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

Copyright terms: Public domain