![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbiran | GIF version |
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.) |
Ref | Expression |
---|---|
mpbiran.1 | ⊢ 𝜓 |
mpbiran.2 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
mpbiran | ⊢ (𝜑 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiran.2 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | mpbiran.1 | . . 3 ⊢ 𝜓 | |
3 | 2 | biantrur 303 | . 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒)) |
4 | 1, 3 | bitr4i 187 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ∧ 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: mpbir2an 942 unssdif 3372 unssin 3376 inssun 3377 invdif 3379 pwpwab 3976 exmidexmid 4198 opabm 4282 regexmidlem1 4534 elirr 4542 en2lp 4555 wessep 4579 peano5 4599 relop 4779 ssrnres 5073 funopab 5253 funcnv2 5278 funcnveq 5281 fnres 5334 idref 5759 rnoprab 5960 elixp 6707 djuf1olem 7054 lbfzo0 10183 txdis1cn 13817 |
Copyright terms: Public domain | W3C validator |