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 1012 rabtru 3674 reueq 3725 ss0b 4348 eusv1 5282 eusv2nf 5286 eusv2 5287 opthprc 5609 sosn 5631 fdmrn 6531 f1cnvcnv 6577 fores 6593 f1orn 6618 funfv 6743 dfoprab2 7201 elxp7 7713 tpostpos 7901 canthwe 10061 opelreal 10540 elreal2 10542 eqresr 10547 elnn1uz2 12313 faclbnd4lem1 13641 isprm2 16014 joindm 17601 meetdm 17615 symgbas0 18451 toptopon 21453 ist1-3 21885 perfcls 21901 prdsxmetlem 22905 rusgrprc 27299 hhsssh2 28974 choc0 29030 chocnul 29032 shlesb1i 29090 adjeu 29593 isarchi 30738 derang0 32313 frrlem11 33030 dfon3 33250 brtxpsd 33252 topmeet 33609 filnetlem2 33624 filnetlem3 33625 bj-rabtrALT 34146 bj-snsetex 34172 relowlpssretop 34527 poimirlem28 34801 fdc 34901 0totbnd 34932 heiborlem3 34972 cossssid 35587 cnvrefrelcoss2 35653 dfdisjALTV 35826 dfeldisj2 35831 dfeldisj3 35832 dfeldisj4 35833 disjxrn 35857 ifpid3g 39736 elintima 39876 |
Copyright terms: Public domain | W3C validator |