![]() |
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 2246 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
4 | 3 | ancoms 268 | 1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1364 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-cleq 2186 |
This theorem is referenced by: sbcied2 3024 csbied2 3129 fun2ssres 5298 fcoi1 5435 fcoi2 5436 funssfv 5581 caovimo 6114 mpomptsx 6252 dmmpossx 6254 fmpox 6255 2ndconst 6277 mpoxopoveq 6295 tfrlemisucaccv 6380 tfr1onlemsucaccv 6396 tfrcllemsucaccv 6409 rdgivallem 6436 nnmass 6542 nnm00 6585 ssenen 6909 fi0 7036 nnnninf2 7188 nnnninfeq2 7190 exmidfodomrlemim 7263 ltexnqq 7470 ltrnqg 7482 nqnq0a 7516 nqnq0m 7517 nq0m0r 7518 nq0a0 7519 addnqprllem 7589 addnqprulem 7590 map2psrprg 7867 rereceu 7951 addid0 8394 nnnn0addcl 9273 zindd 9438 qaddcl 9703 qmulcl 9705 qreccl 9710 xaddpnf1 9915 xaddmnf1 9917 xaddnemnf 9926 xaddnepnf 9927 xaddcom 9930 xnegdi 9937 xaddass 9938 xpncan 9940 xleadd1a 9942 xltadd1 9945 xlt2add 9949 modfzo0difsn 10469 frec2uzrdg 10483 seqf1oglem2 10594 expp1 10620 expnegap0 10621 expcllem 10624 mulexp 10652 expmul 10658 sqoddm1div8 10767 bcpasc 10840 hashfzo 10896 shftfn 10971 reim0b 11009 cjexp 11040 sumsnf 11555 binomlem 11629 prodsnf 11738 ef0lem 11806 dvdsnegb 11954 m1expe 12043 m1expo 12044 m1exp1 12045 flodddiv4 12078 gcdabs 12128 bezoutr1 12173 dvdslcm 12210 lcmeq0 12212 lcmcl 12213 lcmabs 12217 lcmgcdlem 12218 lcmdvds 12220 mulgcddvds 12235 qredeu 12238 divgcdcoprmex 12243 pcge0 12454 pcgcd1 12469 pcadd 12481 pcmpt2 12485 mulgfvalg 13194 mulgnn0subcl 13208 mulgnn0z 13222 f1ghm0to0 13345 srgmulgass 13488 srgpcomp 13489 ringinvnzdiv 13549 lmodvsmmulgdi 13822 znval 14135 isxmet2d 14527 blfvalps 14564 blssioo 14732 efper 14983 relogbcxpbap 15138 logbgcd1irr 15140 lgsdir 15192 lgsne0 15195 lgsdirnn0 15204 lgsdinn0 15205 lgsquadlem2 15235 2lgslem3a 15250 2lgslem3b 15251 2lgslem3c 15252 2lgslem3d 15253 2lgslem3a1 15254 2lgslem3b1 15255 2lgslem3c1 15256 2lgslem3d1 15257 trirec0xor 15605 |
Copyright terms: Public domain | W3C validator |