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

Theorem breqan12d 4462
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 4452 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2an 477 1  |-  ( (
ph  /\  ps )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  breqan12rd  4463  soisores  6212  isoid  6214  isores3  6220  isoini2  6224  ofrfval  6533  fnwelem  6899  fnse  6901  wemaplem1  7972  r0weon  8391  sornom  8658  enqbreq2  9299  nqereu  9308  ordpinq  9322  lterpq  9349  ltresr2  9519  axpre-ltadd  9545  leltadd  10037  lemul1a  10397  negiso  10520  xltneg  11417  lt2sq  12210  le2sq  12211  sqrtle  13060  prdsleval  14735  efgcpbllema  16587  iducn  20613  icopnfhmeo  21270  iccpnfhmeo  21272  xrhmeo  21273  reefiso  22669  sinord  22746  logltb  22809  logccv  22869  atanord  23083  birthdaylem3  23108  lgsquadlem3  23456  mddmd  26993  xrge0iifiso  27668  erdszelem4  28389  erdszelem8  28393  cgrextend  29511  monotuz  30708  monotoddzzfi  30709  expmordi  30714  wepwsolem  30818  fnwe2val  30826  aomclem8  30838  idlaut  35109
  Copyright terms: Public domain W3C validator