Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > breq123d | Structured version Visualization version GIF version |
Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.) |
Ref | Expression |
---|---|
breq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
breq123d.2 | ⊢ (𝜑 → 𝑅 = 𝑆) |
breq123d.3 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
breq123d | ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | breq123d.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
3 | 1, 2 | breq12d 4596 | . 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
4 | breq123d.2 | . . 3 ⊢ (𝜑 → 𝑅 = 𝑆) | |
5 | 4 | breqd 4594 | . 2 ⊢ (𝜑 → (𝐵𝑅𝐷 ↔ 𝐵𝑆𝐷)) |
6 | 3, 5 | bitrd 267 | 1 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑆𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 class class class wbr 4583 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 |
This theorem is referenced by: sbcbr123 4636 fmptco 6303 xpsle 16064 invfuc 16457 yonedainv 16744 opphllem3 25441 lmif 25477 islmib 25479 iscgra 25501 isinag 25529 fmptcof2 28839 submomnd 29041 sgnsv 29058 inftmrel 29065 isinftm 29066 submarchi 29071 suborng 29146 uncov 32560 iscvlat 33628 paddfval 34101 lhpset 34299 tendofset 35064 diaffval 35337 fnwe2val 36637 aomclem8 36649 |
Copyright terms: Public domain | W3C validator |