![]() |
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 528 | . 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒)) |
4 | 1, 3 | bitr4i 270 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 |
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 387 |
This theorem is referenced by: mpbir2an 704 pm5.63 1050 equsexvw 2111 equsexv 2301 equsexALT 2439 ddif 3968 dfun2 4088 dfin2 4089 0pss 4237 pssv 4239 disj4 4249 pwpwab 4834 zfpair 5124 opabn0 5231 relop 5504 ssrnres 5812 funopab 6157 funcnv2 6189 fnres 6239 dffv2 6517 idref 6661 rnoprab 7002 suppssr 7590 brwitnlem 7853 omeu 7931 elixp 8181 1sdom 8431 dfsup2 8618 wemapso2lem 8725 card2inf 8728 harndom 8737 dford2 8793 cantnfp1lem3 8853 cantnfp1 8854 cantnflem1 8862 tz9.12lem3 8928 djulf1o 9050 djurf1o 9051 dfac4 9257 dfac12a 9284 cflem 9382 cfsmolem 9406 dffin7-2 9534 dfacfin7 9535 brdom3 9664 iunfo 9675 gch3 9812 lbfzo0 12802 gcdcllem3 15595 1nprm 15763 cygctb 18645 opsrtoslem2 19844 expmhm 20174 expghm 20203 mat1dimelbas 20644 basdif0 21127 txdis1cn 21808 trfil2 22060 txflf 22179 clsnsg 22282 tgpconncomp 22285 perfdvf 24065 wilthlem3 25208 mptelee 26193 iscplgr 26712 rgrprcx 26889 blocnilem 28213 h1de2i 28966 nmop0 29399 nmfn0 29400 lnopconi 29447 lnfnconi 29468 stcltr2i 29688 funcnvmpt 30015 1stpreima 30031 2ndpreima 30032 suppss3 30049 elmrsubrn 31962 dftr6 32181 br6 32188 dford5reg 32224 txpss3v 32523 brtxp 32525 brpprod 32530 brsset 32534 dfon3 32537 brtxpsd 32539 brtxpsd2 32540 dffun10 32559 elfuns 32560 funpartlem 32587 fullfunfv 32592 dfrdg4 32596 dfint3 32597 brub 32599 hfext 32828 neibastop2lem 32892 bj-equsexval 33173 bj-elid4 33615 finxp0 33772 finxp1o 33773 brvdif 34578 xrnss3v 34681 ntrneiel2 39223 ntrneik4w 39237 compel 39479 funressnvmo 41975 dfdfat2 42029 |
Copyright terms: Public domain | W3C validator |