ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  breq12d GIF version

Theorem breq12d 3912
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 (𝜑𝐴 = 𝐵)
breq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
breq12d (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))

Proof of Theorem breq12d
StepHypRef Expression
1 breq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 breq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 breq12 3904 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 408 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1316   class class class wbr 3899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900
This theorem is referenced by:  breq123d  3913  3brtr3d  3929  3brtr4d  3930  pocl  4195  csbcnvg  4693  cnvpom  5051  sbcfung  5117  isoeq1  5670  isocnv  5680  isotr  5685  caovordig  5904  caovordg  5906  caovord2d  5908  caovord  5910  ofrfval  5958  ofrval  5960  ofrfval2  5966  caofref  5971  fundmeng  6669  xpsneng  6684  xpcomeng  6690  xpdom2g  6694  phplem3g  6718  php5  6720  php5dom  6725  nqtri3or  7172  ltsonq  7174  ltanqg  7176  ltmnqg  7177  lt2addnq  7180  lt2mulnq  7181  prarloclemarch  7194  ltrnqg  7196  ltnnnq  7199  prarloclemlt  7269  addlocprlemgt  7310  mullocprlem  7346  addextpr  7397  recexprlemss1l  7411  recexprlemss1u  7412  recexpr  7414  caucvgprlemcanl  7420  cauappcvgprlemm  7421  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlemlim  7437  cauappcvgpr  7438  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemcl  7452  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgpr  7458  caucvgprprlemell  7461  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemnkeqj  7466  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemloc  7479  caucvgprprlemclphr  7481  caucvgprprlemexb  7483  caucvgprprlem1  7485  lttrsr  7538  ltposr  7539  ltsosr  7540  ltasrg  7546  aptisr  7555  mulextsr1lem  7556  mulextsr1  7557  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffcau  7574  caucvgsrlemoffres  7576  caucvgsr  7578  axpre-ltirr  7658  axpre-ltadd  7662  axpre-mulgt0  7663  axpre-mulext  7664  axcaucvglemcau  7674  axcaucvglemres  7675  ltadd2  8149  ltadd1  8159  leadd2  8161  reapval  8305  reapmul1  8324  remulext2  8329  apreim  8332  apirr  8334  apsym  8335  apcotr  8336  apadd1  8337  apadd2  8338  apneg  8340  mulext1  8341  mulext2  8342  apti  8351  apsub1  8371  subap0  8372  apmul1  8515  apmul2  8516  apdivmuld  8540  ltmul2  8578  lemul2  8579  ltdiv1  8590  ltdiv2  8609  ledivdiv  8612  lediv2  8613  negiso  8677  div4p1lem1div2  8931  qapne  9387  nn0ledivnn  9509  xleadd1  9613  xltadd1  9614  xltadd2  9615  xsubge0  9619  xleaddadd  9625  qtri3or  9975  frecfzennn  10154  monoord  10204  monoord2  10205  leexp1a  10303  bernneq  10367  nn0le2msqd  10420  faclbnd  10442  faclbnd3  10444  faclbnd6  10445  facubnd  10446  fihashdom  10504  zfz1isolemiso  10537  cjap  10633  cvg1nlemcau  10711  cvg1nlemres  10712  resqrexlemlo  10740  resqrexlemcalc3  10743  absext  10790  xrnegiso  10986  xrminltinf  10996  fsumabs  11189  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  addmodlteqALT  11469  nn0seqcvgd  11634  algcvg  11641  algcvga  11644  eucalgcvga  11651  qnumgt0  11787  ctinfomlemom  11851  ispsmet  12403  psmettri2  12408  ismet  12424  isxmet  12425  xmettri2  12441  blvalps  12468  blval  12469  comet  12579  bdxmet  12581  dvef  12767
  Copyright terms: Public domain W3C validator