Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > breqan12d | Structured version Visualization version GIF version |
Description: Equality deduction for a binary relation. (Contributed by NM, 8-Feb-1996.) |
Ref | Expression |
---|---|
breq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
breqan12i.2 | ⊢ (𝜓 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
breqan12d | ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | breqan12i.2 | . 2 ⊢ (𝜓 → 𝐶 = 𝐷) | |
3 | breq12 5058 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
4 | 1, 2, 3 | syl2an 599 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |