Theorem breqan12d 5069

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   class class class wbr 5053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054

This theorem is referenced by:  breqan12rd  5070  soisores  7136  isoid  7138  isores3  7144  isoini2  7148  ofrfvalg  7476  fnwelem  7898  fnse  7900  infsupprpr  9120  wemaplem1  9162  r0weon  9626  sornom  9891  enqbreq2  10534  nqereu  10543  ordpinq  10557  lterpq  10584  ltresr2  10755  axpre-ltadd  10781  leltadd  11316  lemul1a  11686  negiso  11812  xltneg  12807  lt2sq  13704  le2sq  13705  expmordi  13737  sqrtle  14824  prdsleval  16982  efgcpbllema  19144  iducn  23180  icopnfhmeo  23840  iccpnfhmeo  23842  xrhmeo  23843  reefiso  25340  sinord  25423  logltb  25488  logccv  25551  atanord  25810  birthdaylem3  25836  lgsquadlem3  26263  mddmd  30382  xrge0iifiso  31599  revwlkb  32800  erdszelem4  32869  erdszelem8  32873  satfv0  33033  cgrextend  34047  matunitlindf  35512  idlaut  37847  monotuz  40466  monotoddzzfi  40467  wepwsolem  40570  fnwe2val  40577  aomclem8  40589  rrx2plord  45739  rrx2plordisom  45742