Theorem breq12d 4096

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 4088	. 2 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A R C <-> B R D ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  breq123d  4097  3brtr3d  4114  3brtr4d  4115  pocl  4394  csbcnvg  4906  cnvpom  5271  sbcfung  5342  isoeq1  5925  isocnv  5935  isotr  5940  caovordig  6171  caovordg  6173  caovord2d  6175  caovord  6177  ofrfval  6227  ofrval  6229  ofrfval2  6235  caofref  6243  fundmeng  6960  xpsneng  6981  xpcomeng  6987  xpdom2g  6991  phplem3g  7017  php5  7019  php5dom  7024  exmidpw2en  7074  exmidapne  7446  nqtri3or  7583  ltsonq  7585  ltanqg  7587  ltmnqg  7588  lt2addnq  7591  lt2mulnq  7592  prarloclemarch  7605  ltrnqg  7607  ltnnnq  7610  prarloclemlt  7680  addlocprlemgt  7721  mullocprlem  7757  addextpr  7808  recexprlemss1l  7822  recexprlemss1u  7823  recexpr  7825  caucvgprlemcanl  7831  cauappcvgprlemm  7832  cauappcvgprlemdisj  7838  cauappcvgprlemloc  7839  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem1  7846  cauappcvgprlemlim  7848  cauappcvgpr  7849  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemcl  7863  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgpr  7869  caucvgprprlemell  7872  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemnkeqj  7877  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemloc  7890  caucvgprprlemclphr  7892  caucvgprprlemexb  7894  caucvgprprlem1  7896  lttrsr  7949  ltposr  7950  ltsosr  7951  ltasrg  7957  aptisr  7966  mulextsr1lem  7967  mulextsr1  7968  caucvgsrlemcau  7980  caucvgsrlemgt1  7982  caucvgsrlemoffcau  7985  caucvgsrlemoffres  7987  caucvgsr  7989  axpre-ltirr  8069  axpre-ltadd  8073  axpre-mulgt0  8074  axpre-mulext  8075  axcaucvglemcau  8085  axcaucvglemres  8086  ltadd2  8566  ltadd1  8576  leadd2  8578  reapval  8723  reapmul1  8742  remulext2  8747  apreim  8750  apirr  8752  apsym  8753  apcotr  8754  apadd1  8755  apadd2  8756  apneg  8758  mulext1  8759  mulext2  8760  apti  8769  apsub1  8789  subap0  8790  apmul1  8935  apmul2  8936  apdivmuld  8960  ltmul2  9003  lemul2  9004  ltdiv1  9015  ltdiv2  9034  ledivdiv  9037  lediv2  9038  negiso  9102  div4p1lem1div2  9365  qapne  9834  nn0ledivnn  9963  xleadd1  10071  xltadd1  10072  xltadd2  10073  xsubge0  10077  xleaddadd  10083  qtri3or  10460  frecfzennn  10648  monoord  10707  monoord2  10708  leexp1a  10816  bernneq  10882  apexp1  10940  nn0le2msqd  10941  faclbnd  10963  faclbnd3  10965  faclbnd6  10966  facubnd  10967  fihashdom  11025  zfz1isolemiso  11061  cjap  11417  cvg1nlemcau  11495  cvg1nlemres  11496  resqrexlemlo  11524  resqrexlemcalc3  11527  absext  11574  xrnegiso  11773  xrminltinf  11783  fsumabs  11976  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  fprodle  12151  addmodlteqALT  12370  nn0seqcvgd  12563  algcvg  12570  algcvga  12573  eucalgcvga  12580  qnumgt0  12720  pcprendvds2  12814  pcpremul  12816  pcadd2  12864  2expltfac  12962  ctinfomlemom  12998  gsumfzval  13424  mplsubgfilemcl  14663  ispsmet  14997  psmettri2  15002  ismet  15018  isxmet  15019  xmettri2  15035  blvalps  15062  blval  15063  comet  15173  bdxmet  15175  dvef  15401  cxplt  15590  rpcxple2  15592  rpcxplt2  15593  cxplt3  15594  apcxp2  15613  ltexp2  15615  logbleb  15635  logblt  15636  lgsdilem  15706  2lgslem1a2  15766  apdifflemr  16415  apdiff  16416