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 2166 | . 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) | |
2 | eqcoms.1 | . 2 ⊢ (𝐴 = 𝐵 → 𝜑) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ (𝐵 = 𝐴 → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 |
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 1434 ax-gen 1436 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: gencbvex 2767 gencbval 2769 sbceq2a 2956 eqimss2 3192 uneqdifeqim 3489 tppreq3 3673 copsex2t 4217 copsex2g 4218 ordsoexmid 4533 0elsucexmid 4536 ordpwsucexmid 4541 cnveqb 5053 cnveq0 5054 relcoi1 5129 funtpg 5233 f0rn0 5376 f1ocnvfv 5741 f1ocnvfvb 5742 cbvfo 5747 cbvexfo 5748 brabvv 5879 ov6g 5970 ectocld 6558 ecoptocl 6579 phplem3 6811 f1dmvrnfibi 6900 f1vrnfibi 6901 updjud 7038 pr2ne 7139 nn0ind-raph 9299 nn01to3 9546 modqmuladd 10291 modqmuladdnn0 10293 fihashf1rn 10691 hashfzp1 10726 rennim 10930 xrmaxiflemcom 11176 m1expe 11821 m1expo 11822 m1exp1 11823 nn0o1gt2 11827 flodddiv4 11856 cncongr1 12014 m1dvdsndvds 12159 txcn 12822 relogbcxpbap 13430 logbgcd1irr 13432 logbgcd1irraplemexp 13433 bj-inf2vnlem2 13694 |
Copyright terms: Public domain | W3C validator |