New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpbir2an | Unicode version |
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) |
Ref | Expression |
---|---|
mpbir2an.1 | |
mpbir2an.2 | |
mpbiran2an.1 |
Ref | Expression |
---|---|
mpbir2an |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbir2an.2 | . 2 | |
2 | mpbir2an.1 | . . 3 | |
3 | mpbiran2an.1 | . . 3 | |
4 | 2, 3 | mpbiran 884 | . 2 |
5 | 1, 4 | mpbir 200 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wa 358 |
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 177 df-an 360 |
This theorem is referenced by: 3pm3.2i 1130 ax12olem4 1930 euequ1 2292 eqssi 3288 sikss1c1c 4267 ins2kss 4279 ins3kss 4280 cokrelk 4284 cnvkexg 4286 ssetkex 4294 sikexg 4296 ins2kexg 4305 ins3kexg 4306 eqtfinrelk 4486 0ceven 4505 xpvv 4843 fnsn 5152 fnresi 5200 fn0 5202 f0 5248 fconst 5250 f10 5316 f1o0 5319 f1oi 5320 f1ovi 5321 f1osn 5322 fvi 5442 isoid 5490 1stfo 5505 2ndfo 5506 swapf1o 5511 xpassen 6057 2p1e3c 6156 fce 6188 0lt1c 6258 nnltp1c 6262 frecxp 6314 scancan 6331 |
Copyright terms: Public domain | W3C validator |