Theorem cleq12 1113

Description: Equality relationship among 4 classes.

Assertion

Ref	Expression
cleq12	⊢ ((A = B ∧ C = D) → (A = C ↔ B = D))

Proof of Theorem cleq12

Step	Hyp	Ref	Expression
1		cleq1 1107	. 2 ⊢ (A = B → (A = C ↔ B = C))
2		cleq2 1110	. 2 ⊢ (C = D → (B = C ↔ B = D))
3	1, 2	sylan9bb 418	1 ⊢ ((A = B ∧ C = D) → (A = C ↔ B = D))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = wceq 1091

This theorem is referenced by:  cleqfv 2880  tfrlem1 2949  tfrlem2 2950  tfr3 2964  th3qlem1 3250  xpdom2 3345  aceq5lem4 3561  kmlem8 3587  zornlem6 3608  creur 4532  creui 4533  uzind 4603  replimt 4798  xpnnen 4927

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org