![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbiran2 | GIF version |
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.) |
Ref | Expression |
---|---|
mpbiran2.1 | ⊢ 𝜒 |
mpbiran2.2 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
mpbiran2 | ⊢ (𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiran2.2 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | mpbiran2.1 | . . 3 ⊢ 𝜒 | |
3 | 2 | biantru 302 | . 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: reueq 2938 ss0b 3464 eusv1 4454 eusv2nf 4458 eusv2 4459 opthprc 4679 opelres 4914 f1cnvcnv 5434 fores 5449 f1orn 5473 funfvdm 5581 dfoprab2 5924 tpostpos 6267 opelreal 7828 elreal2 7831 eqresr 7837 axprecex 7881 zeoxor 11876 isprm2 12119 toptopon 13557 bdeq0 14658 subctctexmid 14789 |
Copyright terms: Public domain | W3C validator |