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

Theorem breqan12d 4119
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 4109 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A R C  <-> 
B R D ) )
41, 2, 3syl2an 463 1  |-  ( (
ph  /\  ps )  ->  ( A R C  <-> 
B R D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1642   class class class wbr 4104
This theorem is referenced by:  breqan12rd  4120  soisores  5911  isoid  5913  isores3  5919  isoini2  5923  ofrfval  6173  fnwelem  6317  fnse  6319  ovec  6856  wemaplem1  7351  r0weon  7730  sornom  7993  enqbreq2  8634  nqereu  8643  ordpinq  8657  lterpq  8684  ltresr2  8853  axpre-ltadd  8879  leltadd  9348  lemul1a  9700  negiso  9820  xltneg  10636  lt2sq  11270  le2sq  11271  sqrle  11842  prdsleval  13475  efgcpbllema  15162  icopnfhmeo  18545  iccpnfhmeo  18547  xrhmeo  18548  reefiso  19931  sinord  20003  logltb  20061  logccv  20121  atanord  20334  birthdaylem3  20359  lgsquadlem3  20707  mddmd  22995  iducn  23578  erdszelem4  24129  erdszelem8  24133  cgrextend  25190  monotuz  26349  monotoddzzfi  26350  expmordi  26355  wepwsolem  26461  fnwe2val  26469  aomclem8  26482  idlaut  30354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105
  Copyright terms: Public domain W3C validator