Theorem eqeq12 2785

Description: Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
eqeq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Proof of Theorem eqeq12

Step	Hyp	Ref	Expression
1		eqeq1 2776	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqeq2 2783	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷))
3	1, 2	sylan9bb 502	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765

This theorem is referenced by:  eqeq12d  2787  eqeqan12dALT  2789  eqeqan1dOLDOLD  2792  funopg  6216  eqfnfv  6621  2f1fvneq  6837  riotaeqimp  6954  soxp  7622  tfr3  7833  xpdom2  8402  dfac5lem4  9340  kmlem9  9372  sornom  9491  zorn2lem6  9715  elwina  9900  elina  9901  bcn1  13482  summo  14928  prodmo  15144  vdwlem12  16178  pslem  17668  gaorb  18202  gsumval3eu  18772  ringinvnz1ne0  19059  cygznlem3  20412  mat1ov  20755  dmatmulcl  20807  scmatscmiddistr  20815  scmatscm  20820  1mavmul  20855  chmatval  21135  dscmet  22879  dscopn  22880  iundisj2  23847  wlkres  27150  wlkresOLD  27152  wlkp1lem8  27162  1wlkdlem4  27663  frgr2wwlk1  27857  iundisj2f  30100  iundisj2fi  30270  erdszelem9  32031  fununiq  32532  sltval2  32684  bj-elid  33938  unirep  34430  eqeqan2d  34947  csbfv12gALTVD  40652  prproropf1olem4  43036  paireqne  43041  prmdvdsfmtnof1lem2  43115  uspgrsprf1  43390