MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breqan12d Unicode version

Theorem breqan12d 4187
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypotheses
Ref Expression
breq1d.1  |-  ( ph  ->  A  =  B )
breqan12i.2  |-  ( ps 
->  C  =  D
)
Assertion
Ref Expression
breqan12d  |-  ( (
ph  /\  ps )  ->  ( A R C  <-> 
B R D ) )

Proof of Theorem breqan12d
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breqan12i.2 . 2  |-  ( ps 
->  C  =  D
)
3 breq12 4177 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2an 464 1  |-  ( (
ph  /\  ps )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649   class class class wbr 4172
This theorem is referenced by:  breqan12rd  4188  soisores  6006  isoid  6008  isores3  6014  isoini2  6018  ofrfval  6272  fnwelem  6420  fnse  6422  ovec  6973  wemaplem1  7471  r0weon  7850  sornom  8113  enqbreq2  8753  nqereu  8762  ordpinq  8776  lterpq  8803  ltresr2  8972  axpre-ltadd  8998  leltadd  9468  lemul1a  9820  negiso  9940  xltneg  10759  lt2sq  11410  le2sq  11411  sqrle  12021  prdsleval  13654  efgcpbllema  15341  iducn  18266  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  reefiso  20317  sinord  20389  logltb  20447  logccv  20507  atanord  20720  birthdaylem3  20745  lgsquadlem3  21093  mddmd  23757  xrge0iifiso  24274  erdszelem4  24833  erdszelem8  24837  cgrextend  25846  monotuz  26894  monotoddzzfi  26895  expmordi  26900  wepwsolem  27006  fnwe2val  27014  aomclem8  27027  idlaut  30578
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator