![]() |
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 3173 elini 3321 dtruarb 4193 opnzi 4237 so0 4328 we0 4363 ord0 4393 ordon 4487 onsucelsucexmidlem1 4529 regexmidlemm 4533 ordpwsucexmid 4571 reg3exmidlemwe 4580 ordom 4608 funi 5250 funcnvsn 5263 funinsn 5267 fnresi 5335 fn0 5337 f0 5408 fconst 5413 f10 5497 f1o0 5500 f1oi 5501 f1osn 5503 isoid 5813 iso0 5820 acexmidlem2 5874 fo1st 6160 fo2nd 6161 iordsmo 6300 tfrlem7 6320 tfrexlem 6337 mapsnf1o2 6698 1domsn 6821 inresflem 7061 0ct 7108 infnninf 7124 infnninfOLD 7125 exmidonfinlem 7194 exmidaclem 7209 pw1on 7227 sucpw1nel3 7234 1pi 7316 prarloclemcalc 7503 ltsopr 7597 ltsosr 7765 cnm 7833 axicn 7864 axaddf 7869 axmulf 7870 nnindnn 7894 ltso 8037 negiso 8914 nnind 8937 0z 9266 dfuzi 9365 cnref1o 9652 elrpii 9658 xrltso 9798 0e0icopnf 9981 0e0iccpnf 9982 fz0to4untppr 10126 fldiv4p1lem1div2 10307 expcl2lemap 10534 expclzaplem 10546 expge0 10558 expge1 10559 xrnegiso 11272 fclim 11304 eff2 11690 reeff1 11710 ef01bndlem 11766 sin01bnd 11767 cos01bnd 11768 sin01gt0 11771 egt2lt3 11789 halfleoddlt 11901 2prm 12129 3prm 12130 1arith 12367 setsslnid 12516 xpsff1o 12773 isabli 13108 mgpf 13199 zringnzr 13531 fntopon 13563 istpsi 13578 ismeti 13885 tgqioo 14086 addcncntoplem 14090 divcnap 14094 abscncf 14111 recncf 14112 imcncf 14113 cjcncf 14114 dveflem 14226 reeff1o 14233 reefiso 14237 ioocosf1o 14314 lgslem2 14441 lgsfcl2 14446 lgsne0 14478 ex-fl 14516 bj-indint 14722 bj-omord 14751 012of 14784 2o01f 14785 0nninf 14792 peano4nninf 14794 taupi 14860 |
Copyright terms: Public domain | W3C validator |