| 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 530 | . 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒)) |
| 4 | 1, 3 | bitr4i 278 | 1 ⊢ (𝜑 ↔ 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: mpbiran2 710 mpbir2an 711 pm5.63 1022 equsexALT 2424 velcomp 3966 ddif 4141 dfun2 4270 dfin2 4271 0pss 4447 pssv 4449 disj4 4459 pwpwab 5103 zfpair 5421 opabn0 5558 relop 5861 ssrnres 6198 funopab 6601 funcnv2 6634 fnres 6695 dffv2 7004 idref 7166 rnoprab 7538 suppssr 8220 frrlem9 8319 brwitnlem 8545 omeu 8623 naddcllem 8714 elixp 8944 1sdomOLD 9285 dfsup2 9484 card2inf 9595 harndom 9602 dford2 9660 cantnfp1lem3 9720 cantnfp1 9721 cantnflem1 9729 ttrclresv 9757 tz9.12lem3 9829 djulf1o 9952 djurf1o 9953 dfac4 10162 dfac12a 10189 cflem 10285 cflemOLD 10286 cfsmolem 10310 dffin7-2 10438 dfacfin7 10439 brdom3 10568 iunfo 10579 gch3 10716 lbfzo0 13739 fzo1lb 13753 gcdcllem3 16538 1nprm 16716 cygctb 19910 expmhm 21454 expghm 21486 opsrtoslem2 22080 mat1dimelbas 22477 basdif0 22960 txdis1cn 23643 trfil2 23895 txflf 24014 clsnsg 24118 tgpconncomp 24121 perfdvf 25938 wilthlem3 27113 noeta2 27829 etasslt2 27859 made0 27912 noseqind 28298 mptelee 28910 iscplgr 29432 rgrprcx 29610 blocnilem 30823 h1de2i 31572 nmop0 32005 nmfn0 32006 lnopconi 32053 lnfnconi 32074 stcltr2i 32294 funcnvmpt 32677 1stpreima 32716 2ndpreima 32717 suppss3 32735 fmla0 35387 fmlasuc0 35389 elmrsubrn 35525 dftr6 35751 br6 35757 dford5reg 35783 txpss3v 35879 brtxp 35881 brpprod 35886 brsset 35890 dfon3 35893 brtxpsd 35895 brtxpsd2 35896 dffun10 35915 elfuns 35916 funpartlem 35943 fullfunfv 35948 dfrdg4 35952 dfint3 35953 brub 35955 hfext 36184 neibastop2lem 36361 bj-equsexval 36661 bj-elid3 37168 finxp0 37392 finxp1o 37393 brvdif 38262 xrnss3v 38373 ntrneiel2 44099 ntrneik4w 44113 ismnushort 44320 funressnvmo 47057 dfdfat2 47140 |
| Copyright terms: Public domain | W3C validator |