Theorem breqan12d 4669

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

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 |- ( ph -> A = B )
2		breqan12i.2	. 2 |- ( ps -> C = D )
3		breq12 4658	. 2 |- ( ( A = B /\ C = D ) -> ( A R C <-> B R D ) )
4	1, 2, 3	syl2an 494	1 |- ( ( ph /\ ps ) -> ( A R C <-> B R D ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  breqan12rd  4670  soisores  6577  isoid  6579  isores3  6585  isoini2  6589  ofrfval  6905  fnwelem  7292  fnse  7294  wemaplem1  8451  r0weon  8835  sornom  9099  enqbreq2  9742  nqereu  9751  ordpinq  9765  lterpq  9792  ltresr2  9962  axpre-ltadd  9988  leltadd  10512  lemul1a  10877  negiso  11003  xltneg  12048  lt2sq  12937  le2sq  12938  sqrtle  14001  prdsleval  16137  efgcpbllema  18167  iducn  22087  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  reefiso  24202  sinord  24280  logltb  24346  logccv  24409  atanord  24654  birthdaylem3  24680  lgsquadlem3  25107  mddmd  29160  xrge0iifiso  29981  erdszelem4  31176  erdszelem8  31180  cgrextend  32115  matunitlindf  33407  idlaut  35382  monotuz  37506  monotoddzzfi  37507  expmordi  37512  wepwsolem  37612  fnwe2val  37619  aomclem8  37631