![]() |
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 527 | . 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜒)) |
4 | 1, 3 | bitr4i 267 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: pm5.62 996 reueq 3537 ss0b 4108 eusv1 5001 eusv2nf 5005 eusv2 5006 opthprc 5316 sosn 5337 opelresOLD 5553 fdmrn 6217 f1cnvcnv 6262 fores 6277 f1orn 6300 funfv 6419 dfoprab2 6858 elxp7 7360 tpostpos 7533 canthwe 9657 recmulnq 9970 opelreal 10135 elreal2 10137 eqresr 10142 elnn1uz2 11950 faclbnd4lem1 13266 isprm2 15589 joindm 17196 meetdm 17210 symgbas0 18006 efgs1 18340 toptopon 20916 ist1-3 21347 perfcls 21363 prdsxmetlem 22366 rusgrprc 26688 hhsssh2 28428 choc0 28486 chocnul 28488 shlesb1i 28546 adjeu 29049 isarchi 30037 derang0 31450 brtxp 32285 brpprod 32290 dfon3 32297 brtxpsd 32299 topmeet 32657 filnetlem2 32672 filnetlem3 32673 bj-rabtrALT 33225 bj-snsetex 33249 relowlpssretop 33515 poimirlem28 33742 fdc 33846 0totbnd 33877 heiborlem3 33917 cossssid 34532 cnvrefrelcoss2 34598 ifpid3g 38331 elintima 38439 |
Copyright terms: Public domain | W3C validator |