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 285 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
2 | baib.1 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
3 | 1, 2 | syl6rbbr 188 | 1 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: baibr 829 rbaib 830 ceqsrexbv 2675 elrab3 2699 dfpss3 3030 rabsn 3437 elrint2 3656 frind 4089 fnres 5015 f1ompt 5320 fliftfun 5436 ovid 5617 brdifun 6133 xpcomco 6300 ltexprlemdisj 6704 xrlenlt 7084 reapval 7567 znnnlt1 8293 difrp 8619 elfz 8880 fzolb2 9010 elfzo3 9019 fzouzsplit 9035 |
Copyright terms: Public domain | W3C validator |