Theorem breq12d 4143

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Hypotheses

Ref	Expression
breq1d.1	|- ( ph -> A = B )
breq12d.2	|- ( ph -> C = D )

Assertion

Ref	Expression
breq12d	|- ( ph -> ( A R C <-> B R D ) )

Proof of Theorem breq12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breq12d.2	. 2 |- ( ph -> C = D )
3		breq12 4135	. 2 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A R C <-> B R D ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   class class class wbr 4130

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 4131

This theorem is used by:  breq123d  4144  3brtr3d  4161  3brtr4d  4162  pocl  4448  csbcnvg  4964  cnvpom  5330  sbcfung  5401  isoeq1  6007  isocnv  6017  isotr  6022  caovordig  6255  caovordg  6257  caovord2d  6259  caovord  6261  ofrfval  6311  ofrval  6313  ofrfval2  6319  caofref  6327  fundmeng  7095  xpsneng  7120  xpcomeng  7126  xpdom2g  7130  phplem3g  7157  php5  7159  php5dom  7164  exmidpw2en  7219  papirr  7611  exmidapne  7626  nqtri3or  7763  ltsonq  7765  ltanqg  7767  ltmnqg  7768  lt2addnq  7771  lt2mulnq  7772  prarloclemarch  7785  ltrnqg  7787  ltnnnq  7790  prarloclemlt  7860  addlocprlemgt  7901  mullocprlem  7937  addextpr  7988  recexprlemss1l  8002  recexprlemss1u  8003  recexpr  8005  caucvgprlemcanl  8011  cauappcvgprlemm  8012  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexb  8074  caucvgprprlem1  8076  lttrsr  8129  ltposr  8130  ltsosr  8131  ltasrg  8137  aptisr  8146  mulextsr1lem  8147  mulextsr1  8148  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  caucvgsr  8169  axpre-ltirr  8249  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  ltadd2  8748  ltadd1  8758  leadd2  8760  reapval  8906  reapmul1  8925  remulext2  8930  apreim  8933  apirr  8935  apsym  8936  apcotr  8937  apadd1  8938  apadd2  8939  apneg  8941  mulext1  8942  mulext2  8943  apti  8952  apsub1  8972  subap0  8973  apmul1  9120  apmul2  9121  apdivmuld  9145  ltmul2  9188  lemul2  9189  ltdiv1  9200  ltdiv2  9219  ledivdiv  9222  lediv2  9223  negiso  9287  div4p1lem1div2  9563  qapne  10048  nn0ledivnn  10178  xleadd1  10287  xltadd1  10288  xltadd2  10289  xsubge0  10293  xleaddadd  10299  qtri3or  10685  frecfzennn  10876  monoord  10935  monoord2  10936  leexp1a  11044  bernneq  11111  apexp1  11170  nn0le2msqd  11171  faclbnd  11193  faclbnd3  11195  faclbnd6  11196  facubnd  11197  fihashdom  11257  zfz1isolemiso  11305  cjap  11686  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemlo  11793  resqrexlemcalc3  11796  absext  11843  xrnegiso  12044  xrminltinf  12054  fsumabs  12248  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  fprodle  12423  addmodlteqALT  12642  nn0seqcvgd  12835  algcvg  12842  algcvga  12845  eucalgcvga  12852  qnumgt0  12994  pcprendvds2  13090  pcpremul  13092  pcadd2  13140  2expltfac  13239  ctinfomlemom  13367  gzsumfzval  13760  mplsubgfilemcl  15139  ispsmet  15473  psmettri2  15478  ismet  15494  isxmet  15495  xmettri2  15511  blvalps  15538  blval  15539  comet  15649  bdxmet  15651  dvef  15877  cxplt  16071  rpcxple2  16073  rpcxplt2  16074  cxplt3  16075  apcxp2  16094  ltexp2  16096  logbleb  16116  logblt  16117  pellexlem3  16150  ppiqltx  16183  bclbnd  16205  prmefexple  16206  bposlem5  16213  lgsdilem  16244  2lgslem1a2  16304  apdifflemr  17194  apdiff  17195