![]() |
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 534 | . 2 ⊢ (𝜒 ↔ (𝜓 ∧ 𝜒)) |
4 | 1, 3 | bitr4i 281 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: mpbiran2 709 mpbir2an 710 pm5.63 1017 equsexvwOLD 2012 equsexv 2266 equsexALT 2430 velcomp 3896 ddif 4064 dfun2 4186 dfin2 4187 0pss 4352 pssv 4354 disj4 4366 pwpwab 4988 zfpair 5287 opabn0 5405 relop 5685 ssrnres 6002 funopab 6359 funcnv2 6392 fnres 6446 dffv2 6733 idref 6885 rnoprab 7236 suppssr 7844 brwitnlem 8115 omeu 8194 elixp 8451 1sdom 8705 dfsup2 8892 card2inf 9003 harndom 9010 dford2 9067 cantnfp1lem3 9127 cantnfp1 9128 cantnflem1 9136 tz9.12lem3 9202 djulf1o 9325 djurf1o 9326 dfac4 9533 dfac12a 9559 cflem 9657 cfsmolem 9681 dffin7-2 9809 dfacfin7 9810 brdom3 9939 iunfo 9950 gch3 10087 lbfzo0 13072 gcdcllem3 15840 1nprm 16013 cygctb 19005 expmhm 20160 expghm 20189 opsrtoslem2 20724 mat1dimelbas 21076 basdif0 21558 txdis1cn 22240 trfil2 22492 txflf 22611 clsnsg 22715 tgpconncomp 22718 perfdvf 24506 wilthlem3 25655 mptelee 26689 iscplgr 27205 rgrprcx 27382 blocnilem 28587 h1de2i 29336 nmop0 29769 nmfn0 29770 lnopconi 29817 lnfnconi 29838 stcltr2i 30058 funcnvmpt 30430 1stpreima 30466 2ndpreima 30467 suppss3 30486 fmla0 32742 fmlasuc0 32744 elmrsubrn 32880 dftr6 33099 br6 33106 dford5reg 33140 frrlem9 33244 txpss3v 33452 brtxp 33454 brpprod 33459 brsset 33463 dfon3 33466 brtxpsd 33468 brtxpsd2 33469 dffun10 33488 elfuns 33489 funpartlem 33516 fullfunfv 33521 dfrdg4 33525 dfint3 33526 brub 33528 hfext 33757 neibastop2lem 33821 bj-equsexval 34106 bj-elid3 34582 finxp0 34808 finxp1o 34809 brvdif 35682 xrnss3v 35784 ntrneiel2 40789 ntrneik4w 40803 funressnvmo 43637 dfdfat2 43684 |
Copyright terms: Public domain | W3C validator |