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

Theorem breqan12d 4307
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 4297 . 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 1369   class class class wbr 4292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293
This theorem is referenced by:  breqan12rd  4308  soisores  6018  isoid  6020  isores3  6026  isoini2  6030  ofrfval  6328  fnwelem  6687  fnse  6689  ovec  7210  wemaplem1  7760  r0weon  8179  sornom  8446  enqbreq2  9089  nqereu  9098  ordpinq  9112  lterpq  9139  ltresr2  9308  axpre-ltadd  9334  leltadd  9823  lemul1a  10183  negiso  10306  xltneg  11187  lt2sq  11939  le2sq  11940  sqrle  12750  prdsleval  14415  efgcpbllema  16251  iducn  19858  icopnfhmeo  20515  iccpnfhmeo  20517  xrhmeo  20518  reefiso  21913  sinord  21990  logltb  22048  logccv  22108  atanord  22322  birthdaylem3  22347  lgsquadlem3  22695  mddmd  25705  xrge0iifiso  26365  erdszelem4  27082  erdszelem8  27086  cgrextend  28039  monotuz  29282  monotoddzzfi  29283  expmordi  29288  wepwsolem  29394  fnwe2val  29402  aomclem8  29414  idlaut  33740
  Copyright terms: Public domain W3C validator