![]() |
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 | baib.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ibar 301 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr4id 199 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: baibr 920 rbaib 921 ceqsrexbv 2868 elrab3 2894 rabsn 3659 elrint2 3885 frind 4351 fnres 5331 f1ompt 5666 fliftfun 5794 ovid 5988 brdifun 6559 xpcomco 6823 ltexprlemdisj 7602 xrlenlt 8018 reapval 8529 znnnlt1 9297 difrp 9688 elfz 10010 fzolb2 10149 elfzo3 10158 fzouzsplit 10174 rpexp 12145 isabl2 13028 bastop1 13454 cnntr 13596 lmres 13619 tx1cn 13640 tx2cn 13641 xmetec 13808 lgsabs1 14311 |
Copyright terms: Public domain | W3C validator |