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 925 | . 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 1160 euequ1 2101 eqssi 3144 elini 3292 dtruarb 4155 opnzi 4198 so0 4289 we0 4324 ord0 4354 ordon 4448 onsucelsucexmidlem1 4490 regexmidlemm 4494 ordpwsucexmid 4532 reg3exmidlemwe 4541 ordom 4569 funi 5205 funcnvsn 5218 funinsn 5222 fnresi 5290 fn0 5292 f0 5363 fconst 5368 f10 5451 f1o0 5454 f1oi 5455 f1osn 5457 isoid 5763 iso0 5770 acexmidlem2 5824 fo1st 6108 fo2nd 6109 iordsmo 6247 tfrlem7 6267 tfrexlem 6284 mapsnf1o2 6644 1domsn 6767 inresflem 7007 0ct 7054 infnninf 7070 infnninfOLD 7071 exmidonfinlem 7131 exmidaclem 7146 pw1on 7164 sucpw1nel3 7171 1pi 7238 prarloclemcalc 7425 ltsopr 7519 ltsosr 7687 cnm 7755 axicn 7786 axaddf 7791 axmulf 7792 nnindnn 7816 ltso 7958 negiso 8832 nnind 8855 0z 9184 dfuzi 9280 cnref1o 9566 elrpii 9570 xrltso 9710 0e0icopnf 9890 0e0iccpnf 9891 fz0to4untppr 10033 fldiv4p1lem1div2 10214 expcl2lemap 10441 expclzaplem 10453 expge0 10465 expge1 10466 xrnegiso 11171 fclim 11203 eff2 11589 reeff1 11609 ef01bndlem 11665 sin01bnd 11666 cos01bnd 11667 sin01gt0 11670 egt2lt3 11688 halfleoddlt 11798 2prm 12020 3prm 12021 setsslnid 12337 fntopon 12518 istpsi 12533 ismeti 12842 tgqioo 13043 addcncntoplem 13047 divcnap 13051 abscncf 13068 recncf 13069 imcncf 13070 cjcncf 13071 dveflem 13183 reeff1o 13190 reefiso 13194 ioocosf1o 13271 ex-fl 13398 bj-indint 13603 bj-omord 13632 012of 13664 2o01f 13665 0nninf 13673 peano4nninf 13675 taupi 13738 |
Copyright terms: Public domain | W3C validator |