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

Theorem breq12d 3835
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 3827 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1287   class class class wbr 3822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-br 3823
This theorem is referenced by:  breq123d  3836  3brtr3d  3851  3brtr4d  3852  pocl  4106  csbcnvg  4590  cnvpom  4941  sbcfung  5006  isoeq1  5543  isocnv  5553  isotr  5558  caovordig  5769  caovordg  5771  caovord2d  5773  caovord  5775  ofrfval  5823  ofrval  5825  ofrfval2  5830  caofref  5835  fundmeng  6478  xpsneng  6492  xpcomeng  6498  xpdom2g  6502  phplem3g  6526  php5  6528  php5dom  6533  nqtri3or  6902  ltsonq  6904  ltanqg  6906  ltmnqg  6907  lt2addnq  6910  lt2mulnq  6911  prarloclemarch  6924  ltrnqg  6926  ltnnnq  6929  prarloclemlt  6999  addlocprlemgt  7040  mullocprlem  7076  addextpr  7127  recexprlemss1l  7141  recexprlemss1u  7142  recexpr  7144  caucvgprlemcanl  7150  cauappcvgprlemm  7151  cauappcvgprlemdisj  7157  cauappcvgprlemloc  7158  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem1  7165  cauappcvgprlemlim  7167  cauappcvgpr  7168  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemdisj  7180  caucvgprlemloc  7181  caucvgprlemcl  7182  caucvgprlemladdrl  7184  caucvgprlem1  7185  caucvgpr  7188  caucvgprprlemell  7191  caucvgprprlemcbv  7193  caucvgprprlemval  7194  caucvgprprlemnkeqj  7196  caucvgprprlemopl  7203  caucvgprprlemlol  7204  caucvgprprlemloc  7209  caucvgprprlemclphr  7211  caucvgprprlemexb  7213  caucvgprprlem1  7215  lttrsr  7255  ltposr  7256  ltsosr  7257  ltasrg  7263  aptisr  7271  mulextsr1lem  7272  mulextsr1  7273  caucvgsrlemcau  7285  caucvgsrlemgt1  7287  caucvgsrlemoffcau  7290  caucvgsrlemoffres  7292  caucvgsr  7294  axpre-ltirr  7364  axpre-ltadd  7368  axpre-mulgt0  7369  axpre-mulext  7370  axcaucvglemcau  7380  axcaucvglemres  7381  ltadd2  7844  ltadd1  7854  leadd2  7856  reapval  7997  reapmul1  8016  remulext2  8021  apreim  8024  apirr  8026  apsym  8027  apcotr  8028  apadd1  8029  apadd2  8030  apneg  8032  mulext1  8033  mulext2  8034  apti  8043  apmul1  8197  ltmul2  8255  lemul2  8256  ltdiv1  8267  ltdiv2  8286  ledivdiv  8289  lediv2  8290  negiso  8354  div4p1lem1div2  8605  qapne  9059  nn0ledivnn  9173  qtri3or  9585  frecfzennn  9764  monoord  9813  monoord2  9814  leexp1a  9912  bernneq  9974  nn0le2msqd  10027  faclbnd  10049  faclbnd3  10051  faclbnd6  10052  facubnd  10053  fihashdom  10111  zfz1isolemiso  10144  cjap  10239  cvg1nlemcau  10316  cvg1nlemres  10317  resqrexlemlo  10345  resqrexlemcalc3  10348  absext  10395  addmodlteqALT  10766  nn0seqcvgd  10929  ialgcvg  10936  ialgcvga  10939  eucialgcvga  10946  qnumgt0  11082
  Copyright terms: Public domain W3C validator