Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylan9eqr | GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) |
Ref | Expression |
---|---|
sylan9eqr.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
sylan9eqr.2 | ⊢ (𝜓 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
sylan9eqr | ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9eqr.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | sylan9eqr.2 | . . 3 ⊢ (𝜓 → 𝐵 = 𝐶) | |
3 | 1, 2 | sylan9eq 2092 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
4 | 3 | ancoms 255 | 1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 = wceq 1243 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: sbcied2 2800 csbied2 2893 fun2ssres 4943 fcoi1 5070 fcoi2 5071 funssfv 5199 caovimo 5694 mpt2mptsx 5823 dmmpt2ssx 5825 fmpt2x 5826 2ndconst 5843 mpt2xopoveq 5855 tfrlemisucaccv 5939 rdgivallem 5968 nnmass 6066 nnm00 6102 ltexnqq 6506 ltrnqg 6518 nqnq0a 6552 nqnq0m 6553 nq0m0r 6554 nq0a0 6555 addnqprllem 6625 addnqprulem 6626 rereceu 6963 nnnn0addcl 8212 zindd 8356 qaddcl 8570 qmulcl 8572 qreccl 8576 frec2uzrdg 9195 expp1 9262 expnegap0 9263 expcllem 9266 mulexp 9294 expmul 9300 shftfn 9425 reim0b 9462 cjexp 9493 |
Copyright terms: Public domain | W3C validator |