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 301 | . 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒)) |
4 | 1, 3 | bitr4i 186 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ∧ 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: mpbir2an 911 unssdif 3281 unssin 3285 inssun 3286 invdif 3288 pwpwab 3870 exmidexmid 4090 opabm 4172 regexmidlem1 4418 elirr 4426 en2lp 4439 wessep 4462 peano5 4482 relop 4659 ssrnres 4951 funopab 5128 funcnv2 5153 funcnveq 5156 fnres 5209 idref 5626 rnoprab 5822 elixp 6567 djuf1olem 6906 lbfzo0 9913 txdis1cn 12358 |
Copyright terms: Public domain | W3C validator |