Theorem breqan12d 5126

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 5115	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  breqan12rd  5127  soisores  7305  isoid  7307  isores3  7313  isoini2  7317  ofrfvalg  7664  fnwelem  8113  fnse  8115  infsupprpr  9464  wemaplem1  9506  r0weon  9972  sornom  10237  enqbreq2  10880  nqereu  10889  ordpinq  10903  lterpq  10930  ltresr2  11101  axpre-ltadd  11127  leltadd  11669  lemul1a  12043  negiso  12170  xltneg  13184  lt2sq  14105  le2sq  14106  expmordi  14139  sqrtle  15233  prdsleval  17447  efgcpbllema  19691  iducn  24177  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  reefiso  26365  sinord  26450  logltb  26516  logccv  26579  atanord  26844  birthdaylem3  26870  lgsquadlem3  27300  sltneg  27958  onsiso  28176  mddmd  32237  xrge0iifiso  33932  revwlkb  35120  erdszelem4  35188  erdszelem8  35192  satfv0  35352  cgrextend  36003  matunitlindf  37619  idlaut  40097  monotuz  42937  monotoddzzfi  42938  wepwsolem  43038  fnwe2val  43045  aomclem8  43057  isgrlim  47985  rrx2plord  48713  rrx2plordisom  48716