New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > an32s | Unicode version |
Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.) |
Ref | Expression |
---|---|
an32s.1 |
Ref | Expression |
---|---|
an32s |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an32 773 | . 2 | |
2 | an32s.1 | . 2 | |
3 | 1, 2 | sylbi 187 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: anass1rs 782 anabss1 787 ncfinlower 4483 nnadjoin 4520 nnpweq 4523 tfinnn 4534 fssres 5238 foco 5279 f1ores 5300 fun11iun 5305 fconstfv 5456 isocnv 5491 isomin 5496 f1oiso 5499 ncssfin 6151 nntccl 6170 tlecg 6229 ce2le 6232 nnc3n3p1 6276 nchoicelem12 6298 nchoicelem19 6305 |
Copyright terms: Public domain | W3C validator |