Theorem 3brtr4d 4163

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)

Hypotheses

Ref	Expression
3brtr4d.1	⊢ (𝜑 → 𝐴𝑅𝐵)
3brtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3brtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3brtr4d	⊢ (𝜑 → 𝐶𝑅𝐷)

Proof of Theorem 3brtr4d

Step	Hyp	Ref	Expression
1		3brtr4d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3		3brtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	breq12d 4144	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 167	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   class class class wbr 4131

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132

This theorem is used by:  f1oiso2  6036  prarloclemarch2  7792  caucvgprprlemmu  8068  caucvgsrlembound  8167  mulap0  8990  lediv12a  9232  recp1lt1  9237  xleadd1a  10292  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  intfracq  10778  modqmulnn  10800  addmodlteq  10856  frecfzennn  10884  monoord2  10944  expgt1  11035  leexp2r  11051  leexp1a  11052  bernneq  11119  faclbnd  11201  faclbnd6  11204  facubnd  11205  hashunlem  11266  zfz1isolemiso  11313  sqrtgt0  11822  absrele  11872  absimle  11873  abstri  11893  abs2difabs  11897  bdtrilem  12030  bdtri  12031  xrmaxifle  12037  xrmaxadd  12052  xrbdtri  12067  climsqz  12126  climsqz2  12127  fsum3cvg2  12186  isumle  12287  expcnvap0  12294  expcnvre  12295  explecnv  12297  cvgratz  12324  efcllemp  12450  ege2le3  12463  eflegeo  12493  cos12dec  12560  fsumdvds  12634  phibnd  13024  pcdvdstr  13135  pcprmpw2  13141  pockthg  13165  2expltfac  13248  znrrg  15104  psmetres2  15559  xmetres2  15605  comet  15725  bdxmet  15727  cnmet  15756  ivthdec  15870  limcimolemlt  15890  efap1p  16005  tangtx  16065  logbgcd1irraplemap  16205  birthdaylem3  16227  chtqwordi  16263  ppiqwordi  16268  ppiqub  16293  chtqleppi  16294  chtublem  16295  chtqub  16296  bcmono  16304  bclbnd  16307  bposlem1  16311  bposlem6  16316  bposlem9  16319  2lgslem1c  16414  cvgcmp2nlemabs  17287  trilpolemlt1  17297