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 924 | . 2 |
5 | 1, 4 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3pm3.2i 1159 euequ1 2092 eqssi 3108 elini 3255 dtruarb 4110 opnzi 4152 so0 4243 we0 4278 ord0 4308 ordon 4397 onsucelsucexmidlem1 4438 regexmidlemm 4442 ordpwsucexmid 4480 reg3exmidlemwe 4488 ordom 4515 funi 5150 funcnvsn 5163 funinsn 5167 fnresi 5235 fn0 5237 f0 5308 fconst 5313 f10 5394 f1o0 5397 f1oi 5398 f1osn 5400 isoid 5704 iso0 5711 acexmidlem2 5764 fo1st 6048 fo2nd 6049 iordsmo 6187 tfrlem7 6207 tfrexlem 6224 mapsnf1o2 6583 1domsn 6706 inresflem 6938 0ct 6985 infnninf 7015 exmidonfinlem 7042 exmidaclem 7057 1pi 7116 prarloclemcalc 7303 ltsopr 7397 ltsosr 7565 cnm 7633 axicn 7664 axaddf 7669 axmulf 7670 nnindnn 7694 ltso 7835 negiso 8706 nnind 8729 0z 9058 dfuzi 9154 cnref1o 9433 elrpii 9437 xrltso 9575 0e0icopnf 9755 0e0iccpnf 9756 fldiv4p1lem1div2 10071 expcl2lemap 10298 expclzaplem 10310 expge0 10322 expge1 10323 xrnegiso 11024 fclim 11056 eff2 11375 reeff1 11396 ef01bndlem 11452 sin01bnd 11453 cos01bnd 11454 sin01gt0 11457 egt2lt3 11475 halfleoddlt 11580 2prm 11797 3prm 11798 setsslnid 11999 fntopon 12180 istpsi 12195 ismeti 12504 tgqioo 12705 addcncntoplem 12709 divcnap 12713 abscncf 12730 recncf 12731 imcncf 12732 cjcncf 12733 dveflem 12844 ex-fl 12926 bj-indint 13118 bj-omord 13147 0nninf 13186 peano4nninf 13189 isomninnlem 13214 taupi 13228 |
Copyright terms: Public domain | W3C validator |