![]() |
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 205 ∧ 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 206 df-an 396 |
This theorem is referenced by: mpbiran2 709 mpbir2an 710 pm5.63 1018 equsexALT 2414 velcomp 3962 ddif 4135 dfun2 4260 dfin2 4261 0pss 4445 pssv 4447 disj4 4459 pwpwab 5106 zfpair 5421 opabn0 5555 relop 5853 ssrnres 6182 funopab 6588 funcnv2 6621 fnres 6682 dffv2 6993 idref 7155 rnoprab 7524 suppssr 8201 frrlem9 8300 brwitnlem 8528 omeu 8606 naddcllem 8697 elixp 8923 1sdomOLD 9274 dfsup2 9468 card2inf 9579 harndom 9586 dford2 9644 cantnfp1lem3 9704 cantnfp1 9705 cantnflem1 9713 ttrclresv 9741 tz9.12lem3 9813 djulf1o 9936 djurf1o 9937 dfac4 10146 dfac12a 10172 cflem 10270 cfsmolem 10294 dffin7-2 10422 dfacfin7 10423 brdom3 10552 iunfo 10563 gch3 10700 lbfzo0 13705 gcdcllem3 16476 1nprm 16650 cygctb 19847 expmhm 21369 expghm 21401 opsrtoslem2 22000 mat1dimelbas 22386 basdif0 22869 txdis1cn 23552 trfil2 23804 txflf 23923 clsnsg 24027 tgpconncomp 24030 perfdvf 25845 wilthlem3 27015 noeta2 27730 etasslt2 27760 made0 27813 noseqind 28178 mptelee 28719 iscplgr 29241 rgrprcx 29419 blocnilem 30627 h1de2i 31376 nmop0 31809 nmfn0 31810 lnopconi 31857 lnfnconi 31878 stcltr2i 32098 funcnvmpt 32466 1stpreima 32499 2ndpreima 32500 suppss3 32519 fmla0 34992 fmlasuc0 34994 elmrsubrn 35130 dftr6 35345 br6 35351 dford5reg 35378 txpss3v 35474 brtxp 35476 brpprod 35481 brsset 35485 dfon3 35488 brtxpsd 35490 brtxpsd2 35491 dffun10 35510 elfuns 35511 funpartlem 35538 fullfunfv 35543 dfrdg4 35547 dfint3 35548 brub 35550 hfext 35779 neibastop2lem 35844 bj-equsexval 36136 bj-elid3 36646 finxp0 36870 finxp1o 36871 brvdif 37733 xrnss3v 37844 ntrneiel2 43516 ntrneik4w 43530 ismnushort 43738 funressnvmo 46427 dfdfat2 46508 |
Copyright terms: Public domain | W3C validator |