Theorem breqan12d 5164

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  breqan12rd  5165  soisores  7326  isoid  7328  isores3  7334  isoini2  7338  ofrfvalg  7680  fnwelem  8119  fnse  8121  infsupprpr  9501  wemaplem1  9543  r0weon  10009  sornom  10274  enqbreq2  10917  nqereu  10926  ordpinq  10940  lterpq  10967  ltresr2  11138  axpre-ltadd  11164  leltadd  11700  lemul1a  12070  negiso  12196  xltneg  13198  lt2sq  14100  le2sq  14101  expmordi  14134  sqrtle  15209  prdsleval  17425  efgcpbllema  19624  iducn  23795  icopnfhmeo  24466  iccpnfhmeo  24468  xrhmeo  24469  reefiso  25967  sinord  26050  logltb  26115  logccv  26178  atanord  26439  birthdaylem3  26465  lgsquadlem3  26892  sltneg  27529  mddmd  31592  xrge0iifiso  32984  revwlkb  34185  erdszelem4  34254  erdszelem8  34258  satfv0  34418  cgrextend  35049  matunitlindf  36572  idlaut  39053  monotuz  41762  monotoddzzfi  41763  wepwsolem  41866  fnwe2val  41873  aomclem8  41885  rrx2plord  47484  rrx2plordisom  47487