Theorem cnveqd 4872

Description: Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)

Hypothesis

Ref	Expression
cnveqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
cnveqd	|- ( ph -> `' A = `' B )

Proof of Theorem cnveqd

Step	Hyp	Ref	Expression
1		cnveqd.1	. 2 |- ( ph -> A = B )
2		cnveq 4870	. 2 |- ( A = B -> `' A = `' B )
3	1, 2	syl 14	1 |- ( ph -> `' A = `' B )

Syntax hints:   -> wi 4   = wceq 1373   `'ccnv 4692

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-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-in 3180  df-ss 3187  df-br 4060  df-opab 4122  df-cnv 4701

This theorem is referenced by:  cnvsng  5187  cores2  5214  suppssof1  6199  2ndval2  6265  2nd1st  6289  cnvf1olem  6333  brtpos2  6360  dftpos4  6372  tpostpos  6373  tposf12  6378  xpcomco  6946  infeq123d  7144  fsumcnv  11863  fprodcnv  12051  ennnfonelemf1  12904  strslfv3  12993  xpsval  13299  grpinvcnv  13515  grplactcnv  13549  eqglact  13676  isunitd  13983  znval  14513  znle2  14529  txswaphmeolem  14907