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 531 | . 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒)) |
4 | 1, 3 | bitr4i 279 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: mpbiran2 706 mpbir2an 707 pm5.63 1013 equsexvwOLD 2003 equsexv 2259 equsexALT 2432 velcomp 3948 ddif 4110 dfun2 4233 dfin2 4234 0pss 4392 pssv 4394 disj4 4404 pwpwab 5016 zfpair 5312 opabn0 5431 relop 5714 ssrnres 6028 funopab 6383 funcnv2 6415 fnres 6467 dffv2 6749 idref 6900 rnoprab 7246 suppssr 7850 brwitnlem 8121 omeu 8200 elixp 8456 1sdom 8709 dfsup2 8896 card2inf 9007 harndom 9016 dford2 9071 cantnfp1lem3 9131 cantnfp1 9132 cantnflem1 9140 tz9.12lem3 9206 djulf1o 9329 djurf1o 9330 dfac4 9536 dfac12a 9562 cflem 9656 cfsmolem 9680 dffin7-2 9808 dfacfin7 9809 brdom3 9938 iunfo 9949 gch3 10086 lbfzo0 13065 gcdcllem3 15838 1nprm 16011 cygctb 18941 opsrtoslem2 20193 expmhm 20542 expghm 20571 mat1dimelbas 21008 basdif0 21489 txdis1cn 22171 trfil2 22423 txflf 22542 clsnsg 22645 tgpconncomp 22648 perfdvf 24428 wilthlem3 25574 mptelee 26608 iscplgr 27124 rgrprcx 27301 blocnilem 28508 h1de2i 29257 nmop0 29690 nmfn0 29691 lnopconi 29738 lnfnconi 29759 stcltr2i 29979 funcnvmpt 30340 1stpreima 30368 2ndpreima 30369 suppss3 30386 fmla0 32526 fmlasuc0 32528 elmrsubrn 32664 dftr6 32883 br6 32890 dford5reg 32924 frrlem9 33028 txpss3v 33236 brtxp 33238 brpprod 33243 brsset 33247 dfon3 33250 brtxpsd 33252 brtxpsd2 33253 dffun10 33272 elfuns 33273 funpartlem 33300 fullfunfv 33305 dfrdg4 33309 dfint3 33310 brub 33312 hfext 33541 neibastop2lem 33605 bj-equsexval 33890 bj-elid3 34351 finxp0 34554 finxp1o 34555 brvdif 35403 xrnss3v 35504 ntrneiel2 40314 ntrneik4w 40328 funressnvmo 43157 dfdfat2 43204 |
Copyright terms: Public domain | W3C validator |