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

Theorem breq12d 3942
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 3934 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝑅𝐶𝐵𝑅𝐷))
41, 2, 3syl2anc 408 1 (𝜑 → (𝐴𝑅𝐶𝐵𝑅𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1331   class class class wbr 3929
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930
This theorem is referenced by:  breq123d  3943  3brtr3d  3959  3brtr4d  3960  pocl  4225  csbcnvg  4723  cnvpom  5081  sbcfung  5147  isoeq1  5702  isocnv  5712  isotr  5717  caovordig  5936  caovordg  5938  caovord2d  5940  caovord  5942  ofrfval  5990  ofrval  5992  ofrfval2  5998  caofref  6003  fundmeng  6701  xpsneng  6716  xpcomeng  6722  xpdom2g  6726  phplem3g  6750  php5  6752  php5dom  6757  nqtri3or  7216  ltsonq  7218  ltanqg  7220  ltmnqg  7221  lt2addnq  7224  lt2mulnq  7225  prarloclemarch  7238  ltrnqg  7240  ltnnnq  7243  prarloclemlt  7313  addlocprlemgt  7354  mullocprlem  7390  addextpr  7441  recexprlemss1l  7455  recexprlemss1u  7456  recexpr  7458  caucvgprlemcanl  7464  cauappcvgprlemm  7465  cauappcvgprlemdisj  7471  cauappcvgprlemloc  7472  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  cauappcvgprlem1  7479  cauappcvgprlemlim  7481  cauappcvgpr  7482  caucvgprlemnkj  7486  caucvgprlemnbj  7487  caucvgprlemdisj  7494  caucvgprlemloc  7495  caucvgprlemcl  7496  caucvgprlemladdrl  7498  caucvgprlem1  7499  caucvgpr  7502  caucvgprprlemell  7505  caucvgprprlemcbv  7507  caucvgprprlemval  7508  caucvgprprlemnkeqj  7510  caucvgprprlemopl  7517  caucvgprprlemlol  7518  caucvgprprlemloc  7523  caucvgprprlemclphr  7525  caucvgprprlemexb  7527  caucvgprprlem1  7529  lttrsr  7582  ltposr  7583  ltsosr  7584  ltasrg  7590  aptisr  7599  mulextsr1lem  7600  mulextsr1  7601  caucvgsrlemcau  7613  caucvgsrlemgt1  7615  caucvgsrlemoffcau  7618  caucvgsrlemoffres  7620  caucvgsr  7622  axpre-ltirr  7702  axpre-ltadd  7706  axpre-mulgt0  7707  axpre-mulext  7708  axcaucvglemcau  7718  axcaucvglemres  7719  ltadd2  8193  ltadd1  8203  leadd2  8205  reapval  8350  reapmul1  8369  remulext2  8374  apreim  8377  apirr  8379  apsym  8380  apcotr  8381  apadd1  8382  apadd2  8383  apneg  8385  mulext1  8386  mulext2  8387  apti  8396  apsub1  8416  subap0  8417  apmul1  8560  apmul2  8561  apdivmuld  8585  ltmul2  8626  lemul2  8627  ltdiv1  8638  ltdiv2  8657  ledivdiv  8660  lediv2  8661  negiso  8725  div4p1lem1div2  8985  qapne  9443  nn0ledivnn  9566  xleadd1  9670  xltadd1  9671  xltadd2  9672  xsubge0  9676  xleaddadd  9682  qtri3or  10032  frecfzennn  10211  monoord  10261  monoord2  10262  leexp1a  10360  bernneq  10424  nn0le2msqd  10477  faclbnd  10499  faclbnd3  10501  faclbnd6  10502  facubnd  10503  fihashdom  10561  zfz1isolemiso  10594  cjap  10690  cvg1nlemcau  10768  cvg1nlemres  10769  resqrexlemlo  10797  resqrexlemcalc3  10800  absext  10847  xrnegiso  11043  xrminltinf  11053  fsumabs  11246  cvgratnnlemnexp  11305  cvgratnnlemmn  11306  addmodlteqALT  11568  nn0seqcvgd  11733  algcvg  11740  algcvga  11743  eucalgcvga  11750  qnumgt0  11887  ctinfomlemom  11951  ispsmet  12506  psmettri2  12511  ismet  12527  isxmet  12528  xmettri2  12544  blvalps  12571  blval  12572  comet  12682  bdxmet  12684  dvef  12871  cxplt  13015  rpcxple2  13017  rpcxplt2  13018  cxplt3  13019  apdifflemr  13347  apdiff  13348
  Copyright terms: Public domain W3C validator