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 847 | . 2 |
5 | 1, 4 | mpbir 134 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 97 wb 98 |
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 1082 euequ1 1995 eqssi 2961 dtruarb 3942 opnzi 3972 so0 4063 we0 4098 ord0 4128 ordon 4212 onsucelsucexmidlem1 4253 regexmidlemm 4257 ordpwsucexmid 4294 reg3exmidlemwe 4303 ordom 4329 funi 4932 funcnvsn 4945 fnresi 5016 fn0 5018 f0 5080 fconst 5082 f10 5160 f1o0 5163 f1oi 5164 f1osn 5166 isoid 5450 acexmidlem2 5509 fo1st 5784 fo2nd 5785 iordsmo 5912 tfrlem7 5933 tfrexlem 5948 1pi 6413 prarloclemcalc 6600 ltsopr 6694 ltsosr 6849 axicn 6939 nnindnn 6967 ltso 7096 nnind 7930 0z 8256 dfuzi 8348 cnref1o 8582 elrpii 8586 xrltso 8717 0e0icopnf 8848 0e0iccpnf 8849 fldiv4p1lem1div2 9147 expcl2lemap 9267 expclzaplem 9279 expge0 9291 expge1 9292 fclim 9815 ex-fl 9895 bj-indint 10055 bj-omord 10085 |
Copyright terms: Public domain | W3C validator |