![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqcoms | GIF 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 2179 | . 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) | |
2 | eqcoms.1 | . 2 ⊢ (𝐴 = 𝐵 → 𝜑) | |
3 | 1, 2 | sylbi 121 | 1 ⊢ (𝐵 = 𝐴 → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 |
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 1447 ax-gen 1449 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: gencbvex 2783 gencbval 2785 sbceq2a 2973 eqimss2 3210 uneqdifeqim 3508 tppreq3 3694 copsex2t 4241 copsex2g 4242 ordsoexmid 4557 0elsucexmid 4560 ordpwsucexmid 4565 cnveqb 5079 cnveq0 5080 relcoi1 5155 funtpg 5262 f0rn0 5405 f1ocnvfv 5773 f1ocnvfvb 5774 cbvfo 5779 cbvexfo 5780 brabvv 5914 ov6g 6005 ectocld 6594 ecoptocl 6615 phplem3 6847 f1dmvrnfibi 6936 f1vrnfibi 6937 updjud 7074 pr2ne 7184 nn0ind-raph 9346 nn01to3 9593 modqmuladd 10339 modqmuladdnn0 10341 fihashf1rn 10739 hashfzp1 10775 rennim 10982 xrmaxiflemcom 11228 m1expe 11874 m1expo 11875 m1exp1 11876 nn0o1gt2 11880 flodddiv4 11909 cncongr1 12073 m1dvdsndvds 12218 mgmsscl 12659 mndinvmod 12723 ringinvnzdiv 13040 txcn 13408 relogbcxpbap 14016 logbgcd1irr 14018 logbgcd1irraplemexp 14019 zabsle1 14033 bj-inf2vnlem2 14345 |
Copyright terms: Public domain | W3C validator |