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 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 2811 elrab3 2836 rabsn 3585 elrint2 3807 frind 4269 fnres 5234 f1ompt 5564 fliftfun 5690 ovid 5880 brdifun 6449 xpcomco 6713 ltexprlemdisj 7407 xrlenlt 7822 reapval 8331 znnnlt1 9095 difrp 9473 elfz 9789 fzolb2 9924 elfzo3 9933 fzouzsplit 9949 rpexp 11820 bastop1 12241 cnntr 12383 lmres 12406 tx1cn 12427 tx2cn 12428 xmetec 12595 |
Copyright terms: Public domain | W3C validator |