Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > an12s | Structured version Visualization version Unicode version |
Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 838 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.) |
Ref | Expression |
---|---|
an12s.1 |
Ref | Expression |
---|---|
an12s |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an12 838 | . 2 | |
2 | an12s.1 | . 2 | |
3 | 1, 2 | sylbi 207 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 |
This theorem is referenced by: anabsan2 863 1stconst 7265 2ndconst 7266 oecl 7617 oaass 7641 odi 7659 oen0 7666 oeworde 7673 ltexprlem4 9861 iccshftr 12306 iccshftl 12308 iccdil 12310 icccntr 12312 ndvdsadd 15134 eulerthlem2 15487 neips 20917 tx1stc 21453 filuni 21689 ufldom 21766 isch3 28098 unoplin 28779 hmoplin 28801 adjlnop 28945 chirredlem2 29250 btwnconn1lem12 32205 btwnconn1 32208 finxpreclem2 33227 poimirlem25 33434 mblfinlem4 33449 iscringd 33797 unichnidl 33830 |
Copyright terms: Public domain | W3C validator |