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

Theorem breq12d 3806
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
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 breq12 3798 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2anc 403 1  |-  ( ph  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1285   class class class wbr 3793
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794
This theorem is referenced by:  breq123d  3807  3brtr3d  3822  3brtr4d  3823  pocl  4066  csbcnvg  4547  cnvpom  4890  sbcfung  4955  isoeq1  5472  isocnv  5482  isotr  5487  caovordig  5697  caovordg  5699  caovord2d  5701  caovord  5703  ofrfval  5751  ofrval  5753  ofrfval2  5758  caofref  5763  fundmeng  6354  xpsneng  6366  xpcomeng  6372  xpdom2g  6376  phplem3g  6391  php5  6393  php5dom  6398  nqtri3or  6648  ltsonq  6650  ltanqg  6652  ltmnqg  6653  lt2addnq  6656  lt2mulnq  6657  prarloclemarch  6670  ltrnqg  6672  ltnnnq  6675  prarloclemlt  6745  addlocprlemgt  6786  mullocprlem  6822  addextpr  6873  recexprlemss1l  6887  recexprlemss1u  6888  recexpr  6890  caucvgprlemcanl  6896  cauappcvgprlemm  6897  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlemlim  6913  cauappcvgpr  6914  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdrl  6930  caucvgprlem1  6931  caucvgpr  6934  caucvgprprlemell  6937  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnkeqj  6942  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexb  6959  caucvgprprlem1  6961  lttrsr  7001  ltposr  7002  ltsosr  7003  ltasrg  7009  aptisr  7017  mulextsr1lem  7018  mulextsr1  7019  caucvgsrlemcau  7031  caucvgsrlemgt1  7033  caucvgsrlemoffcau  7036  caucvgsrlemoffres  7038  caucvgsr  7040  axpre-ltirr  7110  axpre-ltadd  7114  axpre-mulgt0  7115  axpre-mulext  7116  axcaucvglemcau  7126  axcaucvglemres  7127  ltadd2  7590  ltadd1  7600  leadd2  7602  reapval  7743  reapmul1  7762  remulext2  7767  apreim  7770  apirr  7772  apsym  7773  apcotr  7774  apadd1  7775  apadd2  7776  apneg  7778  mulext1  7779  mulext2  7780  apti  7789  apmul1  7943  ltmul2  8001  lemul2  8002  ltdiv1  8013  ltdiv2  8032  ledivdiv  8035  lediv2  8036  negiso  8100  div4p1lem1div2  8351  qapne  8805  nn0ledivnn  8919  qtri3or  9329  frecfzennn  9508  monoord  9551  monoord2  9552  leexp1a  9628  bernneq  9690  nn0le2msqd  9743  faclbnd  9765  faclbnd3  9767  faclbnd6  9768  facubnd  9769  sizedom  9827  cjap  9931  cvg1nlemcau  10008  cvg1nlemres  10009  resqrexlemlo  10037  resqrexlemcalc3  10040  absext  10087  addmodlteqALT  10404  nn0seqcvgd  10567  ialgcvg  10574  ialgcvga  10577  eucialgcvga  10584
  Copyright terms: Public domain W3C validator