![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > mpbiran | 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 492 | . 2 ⊢ (χ ↔ (ψ ∧ χ)) |
4 | 1, 3 | bitr4i 243 | 1 ⊢ (φ ↔ χ) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ∧ wa 358 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: mpbir2an 886 pm5.63 890 ddif 3398 dfun2 3490 dfin2 3491 0pss 3588 pssv 3590 disj4 3599 cnvkexg 4286 ssetkex 4294 sikexg 4296 ins2kexg 4305 ins3kexg 4306 nnsucelrlem1 4424 ncfinlowerlem1 4482 eqtfinrelk 4486 evenfinex 4503 oddfinex 4504 opabn0 4716 setconslem6 4736 fnres 5199 dmsi 5519 otelins2 5791 composeex 5820 dmpprod 5840 crossex 5850 transex 5910 enmap2 6068 csucex 6259 nmembers1lem1 6268 nchoicelem18 6306 dmfrec 6316 fnfreclem1 6317 |
Copyright terms: Public domain | W3C validator |