![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpbiran | Structured version Visualization version GIF version |
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) |
Ref | Expression |
---|---|
mpbiran.1 | ⊢ 𝜓 |
mpbiran.2 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
mpbiran | ⊢ (𝜑 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiran.2 | . 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | mpbiran.1 | . . 3 ⊢ 𝜓 | |
3 | 2 | biantrur 526 | . 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: mpbir2an 975 pm5.63 979 equsexvw 1978 equsexv 2147 equsexALT 2329 ddif 3775 dfun2 3892 dfin2 3893 0pss 4046 pssv 4049 disj4 4058 pwpwab 4646 zfpair 4934 opabn0 5035 relop 5305 ssrnres 5607 funopab 5961 funcnv2 5995 fnres 6045 dffv2 6310 idref 6539 rnoprab 6785 suppssr 7371 brwitnlem 7632 omeu 7710 elixp 7957 1sdom 8204 dfsup2 8391 wemapso2lem 8498 card2inf 8501 harndom 8510 dford2 8555 cantnfp1lem3 8615 cantnfp1 8616 cantnflem1 8624 tz9.12lem3 8690 dfac4 8983 dfac12a 9008 cflem 9106 cfsmolem 9130 dffin7-2 9258 dfacfin7 9259 brdom3 9388 iunfo 9399 gch3 9536 lbfzo0 12547 gcdcllem3 15270 1nprm 15439 cygctb 18339 opsrtoslem2 19533 expmhm 19863 expghm 19892 mat1dimelbas 20325 basdif0 20805 txdis1cn 21486 trfil2 21738 txflf 21857 clsnsg 21960 tgpconncomp 21963 perfdvf 23712 wilthlem3 24841 mptelee 25820 iscplgr 26366 rgrprcx 26544 blocnilem 27787 h1de2i 28540 nmop0 28973 nmfn0 28974 lnopconi 29021 lnfnconi 29042 stcltr2i 29262 funcnvmptOLD 29595 funcnvmpt 29596 1stpreima 29612 2ndpreima 29613 suppss3 29630 elmrsubrn 31543 dftr6 31766 dfpo2 31771 br6 31773 dford5reg 31811 txpss3v 32110 brsset 32121 dfon3 32124 brtxpsd 32126 brtxpsd2 32127 dffun10 32146 elfuns 32147 funpartlem 32174 fullfunfv 32179 dfrdg4 32183 dfint3 32184 brub 32186 hfext 32415 neibastop2lem 32480 bj-equsexval 32763 finxp0 33358 finxp1o 33359 brvdif 34166 xrnss3v 34274 ntrneiel2 38701 ntrneik4w 38715 compel 38958 dfdfat2 41532 |
Copyright terms: Public domain | W3C validator |