![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > breq12i | Structured version Visualization version GIF version |
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
Ref | Expression |
---|---|
breq1i.1 | ⊢ 𝐴 = 𝐵 |
breq12i.2 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
breq12i | ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | breq12i.2 | . 2 ⊢ 𝐶 = 𝐷 | |
3 | breq12 4878 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
4 | 1, 2, 3 | mp2an 685 | 1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1658 class class class wbr 4873 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-br 4874 |
This theorem is referenced by: 3brtr3g 4906 3brtr4g 4907 caovord2 7106 domunfican 8502 ltsonq 10106 ltanq 10108 ltmnq 10109 prlem934 10170 prlem936 10184 ltsosr 10231 ltasr 10237 ltneg 10852 leneg 10855 inelr 11340 lt2sqi 13246 le2sqi 13247 nn0le2msqi 13347 axlowdimlem6 26246 upgrwlkcompim 26940 clwlkcompbp 27084 mdsldmd1i 29745 divcnvlin 32160 relowlpssretop 33757 fsumlessf 40604 climlimsupcex 40796 liminfltlimsupex 40808 liminflelimsupcex 40824 sge0xaddlem2 41442 eubrdm 41967 iscmgmALT 42707 iscsgrpALT 42709 |
Copyright terms: Public domain | W3C validator |