Theorem eqeq12 2784

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 2775	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2		eqeq2 2782	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷))
3	1, 2	sylan9bb 499	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764

This theorem is referenced by:  eqeq12d  2786  eqeqan12dALT  2788  funopg  6063  eqfnfv  6453  2f1fvneq  6659  riotaeqimp  6776  soxp  7441  tfr3  7648  xpdom2  8211  dfac5lem4  9149  kmlem9  9182  sornom  9301  zorn2lem6  9525  elwina  9710  elina  9711  bcn1  13300  summo  14652  prodmo  14869  vdwlem12  15899  pslem  17410  gaorb  17943  gsumval3eu  18508  ringinvnz1ne0  18796  cygznlem3  20129  mat1ov  20468  dmatmulcl  20520  scmatscmiddistr  20528  scmatscm  20533  1mavmul  20568  chmatval  20850  dscmet  22593  dscopn  22594  iundisj2  23533  wlkres  26798  wlkp1lem8  26808  1wlkdlem4  27316  frgr2wwlk1  27507  iundisj2f  29737  iundisj2fi  29892  erdszelem9  31515  fununiq  32001  sltval2  32142  bj-elid  33418  unirep  33835  eqeqan1d  34344  eqeqan2d  34345  csbfv12gALTVD  39654  prmdvdsfmtnof1lem2  42022  uspgrsprf1  42280