![]() |
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 2142 | . 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) | |
2 | eqcoms.1 | . 2 ⊢ (𝐴 = 𝐵 → 𝜑) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ (𝐵 = 𝐴 → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1332 |
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 1424 ax-gen 1426 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 |
This theorem is referenced by: gencbvex 2735 gencbval 2737 sbceq2a 2923 eqimss2 3157 uneqdifeqim 3453 tppreq3 3634 copsex2t 4175 copsex2g 4176 ordsoexmid 4485 0elsucexmid 4488 ordpwsucexmid 4493 cnveqb 5002 cnveq0 5003 relcoi1 5078 funtpg 5182 f0rn0 5325 f1ocnvfv 5688 f1ocnvfvb 5689 cbvfo 5694 cbvexfo 5695 brabvv 5825 ov6g 5916 ectocld 6503 ecoptocl 6524 phplem3 6756 f1dmvrnfibi 6840 f1vrnfibi 6841 updjud 6975 pr2ne 7065 nn0ind-raph 9192 nn01to3 9436 modqmuladd 10170 modqmuladdnn0 10172 fihashf1rn 10567 hashfzp1 10602 rennim 10806 xrmaxiflemcom 11050 m1expe 11632 m1expo 11633 m1exp1 11634 nn0o1gt2 11638 flodddiv4 11667 cncongr1 11820 txcn 12483 relogbcxpbap 13090 logbgcd1irr 13092 logbgcd1irraplemexp 13093 bj-inf2vnlem2 13340 |
Copyright terms: Public domain | W3C validator |