![]() |
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.2 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | mpbiran2.1 | . . 3 ⊢ 𝜒 | |
3 | 2 | biantru 526 | . 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜒)) |
4 | 1, 3 | bitr4i 270 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 385 |
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 199 df-an 386 |
This theorem is referenced by: pm5.62 1043 reueq 3600 ss0b 4167 eusv1 5059 eusv2nf 5063 eusv2 5064 opthprc 5368 sosn 5391 opelresOLD 5612 elridOLD 5668 fdmrn 6277 f1cnvcnv 6323 fores 6339 f1orn 6364 funfv 6488 dfoprab2 6933 elxp7 7434 tpostpos 7608 canthwe 9759 recmulnq 10072 opelreal 10237 elreal2 10239 eqresr 10244 elnn1uz2 12006 faclbnd4lem1 13329 isprm2 15726 joindm 17315 meetdm 17329 symgbas0 18123 efgs1 18458 toptopon 21047 ist1-3 21479 perfcls 21495 prdsxmetlem 22498 rusgrprc 26832 hhsssh2 28644 choc0 28702 chocnul 28704 shlesb1i 28762 adjeu 29265 isarchi 30244 derang0 31660 dfon3 32504 brtxpsd 32506 topmeet 32863 filnetlem2 32878 filnetlem3 32879 bj-rabtrALT 33413 bj-snsetex 33435 relowlpssretop 33702 poimirlem28 33918 fdc 34020 0totbnd 34051 heiborlem3 34091 cossssid 34703 cnvrefrelcoss2 34769 ifpid3g 38609 elintima 38716 |
Copyright terms: Public domain | W3C validator |