![]() |
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 940 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpbir 146 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3pm3.2i 1175 euequ1 2121 eqssi 3171 elini 3319 dtruarb 4190 opnzi 4234 so0 4325 we0 4360 ord0 4390 ordon 4484 onsucelsucexmidlem1 4526 regexmidlemm 4530 ordpwsucexmid 4568 reg3exmidlemwe 4577 ordom 4605 funi 5247 funcnvsn 5260 funinsn 5264 fnresi 5332 fn0 5334 f0 5405 fconst 5410 f10 5494 f1o0 5497 f1oi 5498 f1osn 5500 isoid 5808 iso0 5815 acexmidlem2 5869 fo1st 6155 fo2nd 6156 iordsmo 6295 tfrlem7 6315 tfrexlem 6332 mapsnf1o2 6693 1domsn 6816 inresflem 7056 0ct 7103 infnninf 7119 infnninfOLD 7120 exmidonfinlem 7189 exmidaclem 7204 pw1on 7222 sucpw1nel3 7229 1pi 7311 prarloclemcalc 7498 ltsopr 7592 ltsosr 7760 cnm 7828 axicn 7859 axaddf 7864 axmulf 7865 nnindnn 7889 ltso 8031 negiso 8908 nnind 8931 0z 9260 dfuzi 9359 cnref1o 9646 elrpii 9652 xrltso 9792 0e0icopnf 9975 0e0iccpnf 9976 fz0to4untppr 10119 fldiv4p1lem1div2 10300 expcl2lemap 10527 expclzaplem 10539 expge0 10551 expge1 10552 xrnegiso 11263 fclim 11295 eff2 11681 reeff1 11701 ef01bndlem 11757 sin01bnd 11758 cos01bnd 11759 sin01gt0 11762 egt2lt3 11780 halfleoddlt 11891 2prm 12119 3prm 12120 1arith 12357 setsslnid 12506 isabli 13034 mgpf 13125 zringnzr 13361 fntopon 13393 istpsi 13408 ismeti 13717 tgqioo 13918 addcncntoplem 13922 divcnap 13926 abscncf 13943 recncf 13944 imcncf 13945 cjcncf 13946 dveflem 14058 reeff1o 14065 reefiso 14069 ioocosf1o 14146 lgslem2 14273 lgsfcl2 14278 lgsne0 14310 ex-fl 14337 bj-indint 14543 bj-omord 14572 012of 14605 2o01f 14606 0nninf 14613 peano4nninf 14615 taupi 14680 |
Copyright terms: Public domain | W3C validator |