Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > baib | Unicode version |
Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.) |
Ref | Expression |
---|---|
baib.1 |
Ref | Expression |
---|---|
baib |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ibar 299 | . 2 | |
2 | baib.1 | . 2 | |
3 | 1, 2 | syl6rbbr 198 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: baibr 905 rbaib 906 ceqsrexbv 2816 elrab3 2841 rabsn 3590 elrint2 3812 frind 4274 fnres 5239 f1ompt 5571 fliftfun 5697 ovid 5887 brdifun 6456 xpcomco 6720 ltexprlemdisj 7414 xrlenlt 7829 reapval 8338 znnnlt1 9102 difrp 9480 elfz 9796 fzolb2 9931 elfzo3 9940 fzouzsplit 9956 rpexp 11831 bastop1 12252 cnntr 12394 lmres 12417 tx1cn 12438 tx2cn 12439 xmetec 12606 |
Copyright terms: Public domain | W3C validator |