Theorem breq12d 4122

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 4114	. 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 4109

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 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  breq123d  4123  3brtr3d  4140  3brtr4d  4141  pocl  4424  csbcnvg  4939  cnvpom  5305  sbcfung  5376  isoeq1  5974  isocnv  5984  isotr  5989  caovordig  6220  caovordg  6222  caovord2d  6224  caovord  6226  ofrfval  6275  ofrval  6277  ofrfval2  6283  caofref  6291  fundmeng  7048  xpsneng  7073  xpcomeng  7079  xpdom2g  7083  phplem3g  7110  php5  7112  php5dom  7117  exmidpw2en  7172  papirr  7560  exmidapne  7574  nqtri3or  7711  ltsonq  7713  ltanqg  7715  ltmnqg  7716  lt2addnq  7719  lt2mulnq  7720  prarloclemarch  7733  ltrnqg  7735  ltnnnq  7738  prarloclemlt  7808  addlocprlemgt  7849  mullocprlem  7885  addextpr  7936  recexprlemss1l  7950  recexprlemss1u  7951  recexpr  7953  caucvgprlemcanl  7959  cauappcvgprlemm  7960  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem1  7974  cauappcvgprlemlim  7976  cauappcvgpr  7977  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgpr  7997  caucvgprprlemell  8000  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnkeqj  8005  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexb  8022  caucvgprprlem1  8024  lttrsr  8077  ltposr  8078  ltsosr  8079  ltasrg  8085  aptisr  8094  mulextsr1lem  8095  mulextsr1  8096  caucvgsrlemcau  8108  caucvgsrlemgt1  8110  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  caucvgsr  8117  axpre-ltirr  8197  axpre-ltadd  8201  axpre-mulgt0  8202  axpre-mulext  8203  axcaucvglemcau  8213  axcaucvglemres  8214  ltadd2  8693  ltadd1  8703  leadd2  8705  reapval  8850  reapmul1  8869  remulext2  8874  apreim  8877  apirr  8879  apsym  8880  apcotr  8881  apadd1  8882  apadd2  8883  apneg  8885  mulext1  8886  mulext2  8887  apti  8896  apsub1  8916  subap0  8917  apmul1  9062  apmul2  9063  apdivmuld  9087  ltmul2  9130  lemul2  9131  ltdiv1  9142  ltdiv2  9161  ledivdiv  9164  lediv2  9165  negiso  9229  div4p1lem1div2  9492  qapne  9971  nn0ledivnn  10100  xleadd1  10208  xltadd1  10209  xltadd2  10210  xsubge0  10214  xleaddadd  10220  qtri3or  10600  frecfzennn  10788  monoord  10847  monoord2  10848  leexp1a  10956  bernneq  11022  apexp1  11080  nn0le2msqd  11081  faclbnd  11103  faclbnd3  11105  faclbnd6  11106  facubnd  11107  fihashdom  11167  zfz1isolemiso  11211  cjap  11591  cvg1nlemcau  11669  cvg1nlemres  11670  resqrexlemlo  11698  resqrexlemcalc3  11701  absext  11748  xrnegiso  11947  xrminltinf  11957  fsumabs  12151  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  fprodle  12326  addmodlteqALT  12545  nn0seqcvgd  12738  algcvg  12745  algcvga  12748  eucalgcvga  12755  qnumgt0  12895  pcprendvds2  12989  pcpremul  12991  pcadd2  13039  2expltfac  13137  ctinfomlemom  13178  gsumfzval  13604  mplsubgfilemcl  14854  ispsmet  15188  psmettri2  15193  ismet  15209  isxmet  15210  xmettri2  15226  blvalps  15253  blval  15254  comet  15364  bdxmet  15366  dvef  15592  cxplt  15781  rpcxple2  15783  rpcxplt2  15784  cxplt3  15785  apcxp2  15804  ltexp2  15806  logbleb  15826  logblt  15827  pellexlem3  15847  lgsdilem  15900  2lgslem1a2  15960  apdifflemr  16831  apdiff  16832