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

Theorem breqan12d 4449
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 4439 . 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 1381   class class class wbr 4434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435
This theorem is referenced by:  breqan12rd  4450  soisores  6205  isoid  6207  isores3  6213  isoini2  6217  ofrfval  6530  fnwelem  6897  fnse  6899  wemaplem1  7971  r0weon  8390  sornom  8657  enqbreq2  9298  nqereu  9307  ordpinq  9321  lterpq  9348  ltresr2  9518  axpre-ltadd  9544  leltadd  10039  lemul1a  10399  negiso  10522  xltneg  11422  lt2sq  12217  le2sq  12218  sqrtle  13070  prdsleval  14748  efgcpbllema  16643  iducn  20656  icopnfhmeo  21313  iccpnfhmeo  21315  xrhmeo  21316  reefiso  22712  sinord  22790  logltb  22853  logccv  22913  atanord  23127  birthdaylem3  23152  lgsquadlem3  23500  mddmd  27089  xrge0iifiso  27787  erdszelem4  28508  erdszelem8  28512  cgrextend  29630  monotuz  30849  monotoddzzfi  30850  expmordi  30855  wepwsolem  30959  fnwe2val  30967  aomclem8  30979  idlaut  35543
  Copyright terms: Public domain W3C validator