Theorem opeq12 3835

Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opeq12	|- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )

Proof of Theorem opeq12

Step	Hyp	Ref	Expression
1		opeq1 3833	. 2 |- ( A = C -> <. A , B >. = <. C , B >. )
2		opeq2 3834	. 2 |- ( B = D -> <. C , B >. = <. C , D >. )
3	1, 2	sylan9eq 2260	1 |- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373   <.cop 3646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652

This theorem is referenced by:  opeq12i  3838  opeq12d  3841  cbvopab  4131  opth  4299  copsex2t  4307  copsex2g  4308  relop  4846  funopg  5324  fsn  5775  fnressn  5793  cbvoprab12  6042  eqopi  6281  f1o2ndf1  6337  tposoprab  6389  brecop  6735  th3q  6750  ecovcom  6752  ecovicom  6753  ecovass  6754  ecoviass  6755  ecovdi  6756  ecovidi  6757  xpf1o  6966  1qec  7536  enq0sym  7580  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  mulnnnq0  7598  distrnq0  7607  mulcomnq0  7608  addassnq0  7610  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  axcnre  8029  fsumcnv  11863  fprodcnv  12051  eucalgval2  12490