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 525 | . 2 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜒)) |
4 | 1, 3 | bitr4i 266 | 1 ⊢ (𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ 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 196 df-an 385 |
This theorem is referenced by: pm5.62 960 reueq 3371 ss0b 3925 eusv1 4786 eusv2nf 4790 eusv2 4791 opthprc 5089 sosn 5111 opelres 5322 fdmrn 5977 f1cnvcnv 6022 fores 6037 f1orn 6060 funfv 6175 dfoprab2 6599 elxp7 7092 tpostpos 7259 canthwe 9352 recmulnq 9665 opelreal 9830 elreal2 9832 eqresr 9837 elnn1uz2 11641 faclbnd4lem1 12942 isprm2 15233 joindm 16826 meetdm 16840 symgbas0 17637 efgs1 17971 toptopon 20548 ist1-3 20963 perfcls 20979 prdsxmetlem 21983 hhsssh2 27511 choc0 27569 chocnul 27571 shlesb1i 27629 adjeu 28132 isarchi 29067 derang0 30405 nofulllem5 31105 brtxp 31157 brpprod 31162 dfon3 31169 brtxpsd 31171 topmeet 31529 filnetlem2 31544 filnetlem3 31545 bj-rabtrALT 32119 bj-snsetex 32144 relowlpssretop 32388 poimirlem28 32607 fdc 32711 0totbnd 32742 heiborlem3 32782 ifpid3g 36856 elintima 36964 rusgrprc 40790 |
Copyright terms: Public domain | W3C validator |