![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpbiran2 | Structured version Visualization version GIF version |
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) |
Ref | Expression |
---|---|
mpbiran2.1 | ⊢ 𝜒 |
mpbiran2.2 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
mpbiran2 | ⊢ (𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiran2.1 | . 2 ⊢ 𝜒 | |
2 | mpbiran2.2 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
3 | 2 | biancomi 463 | . 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓)) |
4 | 1, 3 | mpbiran 705 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: pm5.62 1013 rabtru 3615 reueq 3662 ss0b 4271 eusv1 5183 eusv2nf 5187 eusv2 5188 opthprc 5502 sosn 5524 fdmrn 6406 f1cnvcnv 6452 fores 6468 f1orn 6493 funfv 6617 dfoprab2 7071 elxp7 7580 tpostpos 7763 canthwe 9919 opelreal 10398 elreal2 10400 eqresr 10405 elnn1uz2 12174 faclbnd4lem1 13503 isprm2 15855 joindm 17442 meetdm 17456 symgbas0 18253 toptopon 21209 ist1-3 21641 perfcls 21657 prdsxmetlem 22661 rusgrprc 27055 hhsssh2 28738 choc0 28794 chocnul 28796 shlesb1i 28854 adjeu 29357 isarchi 30449 derang0 32025 frrlem11 32743 dfon3 32963 brtxpsd 32965 topmeet 33322 filnetlem2 33337 filnetlem3 33338 bj-rabtrALT 33824 bj-snsetex 33899 relowlpssretop 34195 poimirlem28 34470 fdc 34571 0totbnd 34602 heiborlem3 34642 cossssid 35257 cnvrefrelcoss2 35323 dfdisjALTV 35496 dfeldisj2 35501 dfeldisj3 35502 dfeldisj4 35503 disjxrn 35527 ifpid3g 39362 elintima 39502 |
Copyright terms: Public domain | W3C validator |