![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > baib | GIF 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 297 | . 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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: baibr 886 rbaib 887 ceqsrexbv 2784 elrab3 2808 rabsn 3554 elrint2 3776 frind 4232 fnres 5195 f1ompt 5523 fliftfun 5649 ovid 5839 brdifun 6408 xpcomco 6671 ltexprlemdisj 7356 xrlenlt 7747 reapval 8250 znnnlt1 9000 difrp 9373 elfz 9683 fzolb2 9818 elfzo3 9827 fzouzsplit 9843 rpexp 11671 bastop1 12089 cnntr 12230 lmres 12253 tx1cn 12274 tx2cn 12275 xmetec 12420 |
Copyright terms: Public domain | W3C validator |