![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbir2an | GIF 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 2095 eqssi 3118 elini 3265 dtruarb 4123 opnzi 4165 so0 4256 we0 4291 ord0 4321 ordon 4410 onsucelsucexmidlem1 4451 regexmidlemm 4455 ordpwsucexmid 4493 reg3exmidlemwe 4501 ordom 4528 funi 5163 funcnvsn 5176 funinsn 5180 fnresi 5248 fn0 5250 f0 5321 fconst 5326 f10 5409 f1o0 5412 f1oi 5413 f1osn 5415 isoid 5719 iso0 5726 acexmidlem2 5779 fo1st 6063 fo2nd 6064 iordsmo 6202 tfrlem7 6222 tfrexlem 6239 mapsnf1o2 6598 1domsn 6721 inresflem 6953 0ct 7000 infnninf 7030 exmidonfinlem 7066 exmidaclem 7081 1pi 7147 prarloclemcalc 7334 ltsopr 7428 ltsosr 7596 cnm 7664 axicn 7695 axaddf 7700 axmulf 7701 nnindnn 7725 ltso 7866 negiso 8737 nnind 8760 0z 9089 dfuzi 9185 cnref1o 9469 elrpii 9473 xrltso 9612 0e0icopnf 9792 0e0iccpnf 9793 fldiv4p1lem1div2 10109 expcl2lemap 10336 expclzaplem 10348 expge0 10360 expge1 10361 xrnegiso 11063 fclim 11095 eff2 11423 reeff1 11443 ef01bndlem 11499 sin01bnd 11500 cos01bnd 11501 sin01gt0 11504 egt2lt3 11522 halfleoddlt 11627 2prm 11844 3prm 11845 setsslnid 12049 fntopon 12230 istpsi 12245 ismeti 12554 tgqioo 12755 addcncntoplem 12759 divcnap 12763 abscncf 12780 recncf 12781 imcncf 12782 cjcncf 12783 dveflem 12895 reeff1o 12902 reefiso 12906 ioocosf1o 12983 ex-fl 13108 bj-indint 13300 bj-omord 13329 012of 13363 2o01f 13364 0nninf 13372 peano4nninf 13375 taupi 13430 |
Copyright terms: Public domain | W3C validator |