Theorem breqan12d 4820

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   class class class wbr 4804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805

This theorem is referenced by:  breqan12rd  4821  soisores  6741  isoid  6743  isores3  6749  isoini2  6753  ofrfval  7071  fnwelem  7461  fnse  7463  wemaplem1  8618  r0weon  9045  sornom  9311  enqbreq2  9954  nqereu  9963  ordpinq  9977  lterpq  10004  ltresr2  10174  axpre-ltadd  10200  leltadd  10724  lemul1a  11089  negiso  11215  xltneg  12261  lt2sq  13151  le2sq  13152  sqrtle  14220  prdsleval  16359  efgcpbllema  18387  iducn  22308  icopnfhmeo  22963  iccpnfhmeo  22965  xrhmeo  22966  reefiso  24421  sinord  24500  logltb  24566  logccv  24629  atanord  24874  birthdaylem3  24900  lgsquadlem3  25327  mddmd  29490  xrge0iifiso  30311  erdszelem4  31504  erdszelem8  31508  cgrextend  32442  matunitlindf  33738  idlaut  35903  monotuz  38026  monotoddzzfi  38027  expmordi  38032  wepwsolem  38132  fnwe2val  38139  aomclem8  38151