![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbir2an | Unicode version |
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.) |
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 846 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpbir 134 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3pm3.2i 1081 euequ1 1992 eqssi 2955 dtruarb 3933 opnzi 3963 so0 4054 ord0 4094 ordon 4178 onsucelsucexmidlem1 4213 regexmidlemm 4217 ordpwsucexmid 4246 ordom 4272 funi 4875 funcnvsn 4888 fnresi 4959 fn0 4961 f0 5023 fconst 5025 f10 5103 f1o0 5106 f1oi 5107 f1osn 5109 isoid 5393 acexmidlem2 5452 fo1st 5726 fo2nd 5727 iordsmo 5853 tfrlem7 5874 tfrexlem 5889 1pi 6299 prarloclemcalc 6485 ltsopr 6570 ltsosr 6692 axicn 6749 ltso 6893 nnind 7711 0z 8032 dfuzi 8124 cnref1o 8357 elrpii 8361 xrltso 8487 0e0icopnf 8618 0e0iccpnf 8619 expcl2lemap 8921 expclzaplem 8933 expge0 8945 expge1 8946 bj-indint 9390 bj-omord 9420 |
Copyright terms: Public domain | W3C validator |