Theorem breq12d 4121

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 4113	. 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 1398   class class class wbr 4108

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-sn 3694  df-pr 3695  df-op 3697  df-br 4109

This theorem is referenced by:  breq123d  4122  3brtr3d  4139  3brtr4d  4140  pocl  4423  csbcnvg  4938  cnvpom  5304  sbcfung  5375  isoeq1  5973  isocnv  5983  isotr  5988  caovordig  6219  caovordg  6221  caovord2d  6223  caovord  6225  ofrfval  6274  ofrval  6276  ofrfval2  6282  caofref  6290  fundmeng  7047  xpsneng  7072  xpcomeng  7078  xpdom2g  7082  phplem3g  7109  php5  7111  php5dom  7116  exmidpw2en  7171  papirr  7559  exmidapne  7573  nqtri3or  7710  ltsonq  7712  ltanqg  7714  ltmnqg  7715  lt2addnq  7718  lt2mulnq  7719  prarloclemarch  7732  ltrnqg  7734  ltnnnq  7737  prarloclemlt  7807  addlocprlemgt  7848  mullocprlem  7884  addextpr  7935  recexprlemss1l  7949  recexprlemss1u  7950  recexpr  7952  caucvgprlemcanl  7958  cauappcvgprlemm  7959  cauappcvgprlemdisj  7965  cauappcvgprlemloc  7966  cauappcvgprlemladdru  7970  cauappcvgprlemladdrl  7971  cauappcvgprlem1  7973  cauappcvgprlemlim  7975  cauappcvgpr  7976  caucvgprlemnkj  7980  caucvgprlemnbj  7981  caucvgprlemdisj  7988  caucvgprlemloc  7989  caucvgprlemcl  7990  caucvgprlemladdrl  7992  caucvgprlem1  7993  caucvgpr  7996  caucvgprprlemell  7999  caucvgprprlemcbv  8001  caucvgprprlemval  8002  caucvgprprlemnkeqj  8004  caucvgprprlemopl  8011  caucvgprprlemlol  8012  caucvgprprlemloc  8017  caucvgprprlemclphr  8019  caucvgprprlemexb  8021  caucvgprprlem1  8023  lttrsr  8076  ltposr  8077  ltsosr  8078  ltasrg  8084  aptisr  8093  mulextsr1lem  8094  mulextsr1  8095  caucvgsrlemcau  8107  caucvgsrlemgt1  8109  caucvgsrlemoffcau  8112  caucvgsrlemoffres  8114  caucvgsr  8116  axpre-ltirr  8196  axpre-ltadd  8200  axpre-mulgt0  8201  axpre-mulext  8202  axcaucvglemcau  8212  axcaucvglemres  8213  ltadd2  8692  ltadd1  8702  leadd2  8704  reapval  8849  reapmul1  8868  remulext2  8873  apreim  8876  apirr  8878  apsym  8879  apcotr  8880  apadd1  8881  apadd2  8882  apneg  8884  mulext1  8885  mulext2  8886  apti  8895  apsub1  8915  subap0  8916  apmul1  9061  apmul2  9062  apdivmuld  9086  ltmul2  9129  lemul2  9130  ltdiv1  9141  ltdiv2  9160  ledivdiv  9163  lediv2  9164  negiso  9228  div4p1lem1div2  9491  qapne  9970  nn0ledivnn  10099  xleadd1  10207  xltadd1  10208  xltadd2  10209  xsubge0  10213  xleaddadd  10219  qtri3or  10599  frecfzennn  10787  monoord  10846  monoord2  10847  leexp1a  10955  bernneq  11021  apexp1  11079  nn0le2msqd  11080  faclbnd  11102  faclbnd3  11104  faclbnd6  11105  facubnd  11106  fihashdom  11165  zfz1isolemiso  11207  cjap  11587  cvg1nlemcau  11665  cvg1nlemres  11666  resqrexlemlo  11694  resqrexlemcalc3  11697  absext  11744  xrnegiso  11943  xrminltinf  11953  fsumabs  12147  cvgratnnlemnexp  12206  cvgratnnlemmn  12207  fprodle  12322  addmodlteqALT  12541  nn0seqcvgd  12734  algcvg  12741  algcvga  12744  eucalgcvga  12751  qnumgt0  12891  pcprendvds2  12985  pcpremul  12987  pcadd2  13035  2expltfac  13133  ctinfomlemom  13170  gsumfzval  13596  mplsubgfilemcl  14846  ispsmet  15180  psmettri2  15185  ismet  15201  isxmet  15202  xmettri2  15218  blvalps  15245  blval  15246  comet  15356  bdxmet  15358  dvef  15584  cxplt  15773  rpcxple2  15775  rpcxplt2  15776  cxplt3  15777  apcxp2  15796  ltexp2  15798  logbleb  15818  logblt  15819  pellexlem3  15839  lgsdilem  15892  2lgslem1a2  15952  apdifflemr  16823  apdiff  16824