![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE 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 | ⊢ (A = B → φ) |
Ref | Expression |
---|---|
eqcoms | ⊢ (B = A → φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2355 | . 2 ⊢ (B = A ↔ A = B) | |
2 | eqcoms.1 | . 2 ⊢ (A = B → φ) | |
3 | 1, 2 | sylbi 187 | 1 ⊢ (B = A → φ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1642 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-cleq 2346 |
This theorem is referenced by: gencbvex 2901 sbceq2a 3057 sbcco2 3069 eqimss2 3324 uneqdifeq 3638 iotaval 4350 nnsucelr 4428 phi11 4596 phi011 4599 copsex2t 4608 copsex2g 4609 f1ocnvfv 5478 f1ocnvfvb 5479 ov6g 5600 ectocld 5991 ecoptocl 5996 enprmaplem5 6080 ncelncs 6120 1cnc 6139 ncslesuc 6267 |
Copyright terms: Public domain | W3C validator |