![]() |
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 | baib.1 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | ibar 301 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | bitr4id 199 | 1 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
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 921 rbaib 922 ceqsrexbv 2883 elrab3 2909 rabsn 3674 elrint2 3900 frind 4370 fnres 5351 f1ompt 5688 fliftfun 5818 ovid 6013 brdifun 6586 xpcomco 6852 ltexprlemdisj 7635 xrlenlt 8052 reapval 8563 znnnlt1 9331 difrp 9722 elfz 10044 fzolb2 10184 elfzo3 10193 fzouzsplit 10209 rpexp 12185 isghm3 13183 isabl2 13233 dfrhm2 13504 bastop1 14043 cnntr 14185 lmres 14208 tx1cn 14229 tx2cn 14230 xmetec 14397 lgsabs1 14901 |
Copyright terms: Public domain | W3C validator |