Theorem breqan12d 4984

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1525   class class class wbr 4968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969

This theorem is referenced by:  breqan12rd  4985  soisores  6950  isoid  6952  isores3  6958  isoini2  6962  ofrfval  7282  fnwelem  7685  fnse  7687  infsupprpr  8821  wemaplem1  8863  r0weon  9291  sornom  9552  enqbreq2  10195  nqereu  10204  ordpinq  10218  lterpq  10245  ltresr2  10416  axpre-ltadd  10442  leltadd  10978  lemul1a  11348  negiso  11475  xltneg  12464  lt2sq  13352  le2sq  13353  expmordi  13385  sqrtle  14458  prdsleval  16583  efgcpbllema  18611  iducn  22579  icopnfhmeo  23234  iccpnfhmeo  23236  xrhmeo  23237  reefiso  24723  sinord  24803  logltb  24868  logccv  24931  atanord  25190  birthdaylem3  25217  lgsquadlem3  25644  mddmd  29765  xrge0iifiso  30791  revwlkb  31982  erdszelem4  32051  erdszelem8  32055  satfv0  32215  cgrextend  33080  matunitlindf  34442  idlaut  36784  monotuz  39044  monotoddzzfi  39045  wepwsolem  39148  fnwe2val  39155  aomclem8  39167  rrx2plord  44210  rrx2plordisom  44213