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 5063 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
4 | 1, 2, 3 | syl2an 595 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 class class class wbr 5058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 |
This theorem is referenced by: breqan12rd 5075 soisores 7069 isoid 7071 isores3 7077 isoini2 7081 ofrfval 7406 fnwelem 7816 fnse 7818 infsupprpr 8957 wemaplem1 8999 r0weon 9427 sornom 9688 enqbreq2 10331 nqereu 10340 ordpinq 10354 lterpq 10381 ltresr2 10552 axpre-ltadd 10578 leltadd 11113 lemul1a 11483 negiso 11610 xltneg 12600 lt2sq 13488 le2sq 13489 expmordi 13521 sqrtle 14610 prdsleval 16740 efgcpbllema 18811 iducn 22821 icopnfhmeo 23476 iccpnfhmeo 23478 xrhmeo 23479 reefiso 24965 sinord 25045 logltb 25110 logccv 25173 atanord 25432 birthdaylem3 25459 lgsquadlem3 25886 mddmd 30006 xrge0iifiso 31078 revwlkb 32270 erdszelem4 32339 erdszelem8 32343 satfv0 32503 cgrextend 33367 matunitlindf 34772 idlaut 37114 monotuz 39418 monotoddzzfi 39419 wepwsolem 39522 fnwe2val 39529 aomclem8 39541 rrx2plord 44605 rrx2plordisom 44608 |
Copyright terms: Public domain | W3C validator |