Theorem breqan12d 5127

Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.)

Hypotheses

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
breqan12i.2	⊢ (𝜓 → 𝐶 = 𝐷)

Assertion

Ref	Expression
breqan12d	⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Proof of Theorem breqan12d

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breqan12i.2	. 2 ⊢ (𝜓 → 𝐶 = 𝐷)
3		breq12 5116	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2an 607	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  breqan12rd  5128  soisores  7326  isoid  7328  isores3  7334  isoini2  7338  ofrfvalg  7683  fnwelem  8127  fnse  8129  infsupprpr  9466  wemaplem1  9508  r0weon  9996  sornom  10261  enqbreq2  10905  nqereu  10914  ordpinq  10928  lterpq  10955  ltresr2  11126  axpre-ltadd  11152  leltadd  11698  lemul1a  12069  negiso  12195  xltneg  13243  lt2sq  14169  le2sq  14170  expmordi  14203  sqrtle  15311  prdsleval  17530  efgcpbllema  19824  iducn  24408  icopnfhmeo  25071  iccpnfhmeo  25073  xrhmeo  25074  reefiso  26577  sinord  26665  logltb  26731  logccv  26794  atanord  27058  birthdaylem3  27084  lgsquadlem3  27512  ltnegs  28204  oniso  28430  mddmd  32594  xrge0iifiso  34270  revwlkb  35551  erdszelem4  35619  erdszelem8  35623  satfv0  35783  cgrextend  36433  matunitlindf  38192  idlaut  40795  monotuz  43595  monotoddzzfi  43596  wepwsolem  43696  fnwe2val  43703  aomclem8  43715  hashomiso  45661  isgrlim  48671  rrx2plord  49420  rrx2plordisom  49423