Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqcoms | Unicode version |
Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqcoms.1 |
Ref | Expression |
---|---|
eqcoms |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2119 | . 2 | |
2 | eqcoms.1 | . 2 | |
3 | 1, 2 | sylbi 120 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: gencbvex 2706 gencbval 2708 sbceq2a 2892 eqimss2 3122 uneqdifeqim 3418 tppreq3 3596 copsex2t 4137 copsex2g 4138 ordsoexmid 4447 0elsucexmid 4450 ordpwsucexmid 4455 cnveqb 4964 cnveq0 4965 relcoi1 5040 funtpg 5144 f0rn0 5287 f1ocnvfv 5648 f1ocnvfvb 5649 cbvfo 5654 cbvexfo 5655 brabvv 5785 ov6g 5876 ectocld 6463 ecoptocl 6484 phplem3 6716 f1dmvrnfibi 6800 f1vrnfibi 6801 updjud 6935 pr2ne 7016 nn0ind-raph 9136 nn01to3 9377 modqmuladd 10107 modqmuladdnn0 10109 fihashf1rn 10503 hashfzp1 10538 rennim 10742 xrmaxiflemcom 10986 m1expe 11523 m1expo 11524 m1exp1 11525 nn0o1gt2 11529 flodddiv4 11558 cncongr1 11711 txcn 12371 bj-inf2vnlem2 13096 |
Copyright terms: Public domain | W3C validator |