![]() |
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 889 | . 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-1 5 ax-2 6 ax-mp 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 1124 euequ1 2050 eqssi 3055 elini 3199 dtruarb 4047 opnzi 4086 so0 4177 we0 4212 ord0 4242 ordon 4331 onsucelsucexmidlem1 4372 regexmidlemm 4376 ordpwsucexmid 4414 reg3exmidlemwe 4422 ordom 4449 funi 5080 funcnvsn 5093 funinsn 5097 fnresi 5165 fn0 5167 f0 5236 fconst 5241 f10 5322 f1o0 5325 f1oi 5326 f1osn 5328 isoid 5627 iso0 5634 acexmidlem2 5687 fo1st 5966 fo2nd 5967 iordsmo 6100 tfrlem7 6120 tfrexlem 6137 mapsnf1o2 6493 1domsn 6615 inresflem 6832 0ct 6869 infnninf 6893 1pi 6971 prarloclemcalc 7158 ltsopr 7252 ltsosr 7407 axicn 7497 nnindnn 7525 ltso 7660 negiso 8513 nnind 8536 0z 8859 dfuzi 8955 cnref1o 9232 elrpii 9236 xrltso 9365 0e0icopnf 9545 0e0iccpnf 9546 fldiv4p1lem1div2 9861 expcl2lemap 10082 expclzaplem 10094 expge0 10106 expge1 10107 xrnegiso 10805 fclim 10837 eff2 11119 reeff1 11140 ef01bndlem 11196 sin01bnd 11197 cos01bnd 11198 sin01gt0 11201 egt2lt3 11216 halfleoddlt 11321 2prm 11536 3prm 11537 setsslnid 11694 fntopon 11874 istpsi 11889 ismeti 12132 tgqioo 12321 abscncf 12338 recncf 12339 imcncf 12340 cjcncf 12341 ex-fl 12360 bj-indint 12534 bj-omord 12563 0nninf 12598 peano4nninf 12601 |
Copyright terms: Public domain | W3C validator |