![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpbiran2 | Structured version Visualization version Unicode 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 512 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitr4i 260 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 df-an 377 |
This theorem is referenced by: pm5.62 939 reueq 3248 ss0b 3776 eusv1 4614 eusv2nf 4618 eusv2 4619 opthprc 4904 sosn 4926 opelres 5132 fdmrn 5771 f1cnvcnv 5814 fores 5829 f1orn 5851 funfv 5960 dfoprab2 6369 elxp7 6858 tpostpos 7024 canthwe 9107 recmulnq 9420 opelreal 9585 elreal2 9587 eqresr 9592 elnn1uz2 11269 faclbnd4lem1 12516 isprm2 14687 joindm 16304 meetdm 16318 symgbas0 17090 efgs1 17440 toptopon 20003 ist1-3 20420 perfcls 20436 prdsxmetlem 21438 hhsssh2 26977 choc0 27035 chocnul 27037 shlesb1i 27095 adjeu 27598 isarchi 28550 derang0 29942 nofulllem5 30645 brtxp 30697 brpprod 30702 dfon3 30709 brtxpsd 30711 topmeet 31070 filnetlem2 31085 filnetlem3 31086 bj-rabtrALT 31580 bj-snsetex 31603 relowlpssretop 31813 poimirlem28 32014 fdc 32120 0totbnd 32151 heiborlem3 32191 ifpid3g 36182 elintima 36291 rusgrprc 39751 |
Copyright terms: Public domain | W3C validator |