![]() |
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 942 | . 2 ⊢ (𝜑 ↔ 𝜒) |
5 | 1, 4 | mpbir 146 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 |
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 1177 euequ1 2133 eqssi 3186 elini 3334 dtruarb 4209 opnzi 4253 so0 4344 we0 4379 ord0 4409 ordon 4503 onsucelsucexmidlem1 4545 regexmidlemm 4549 ordpwsucexmid 4587 reg3exmidlemwe 4596 ordom 4624 funi 5267 funcnvsn 5280 funinsn 5284 fnresi 5352 fn0 5354 f0 5425 fconst 5430 f10 5514 f1o0 5517 f1oi 5518 f1osn 5520 isoid 5832 iso0 5839 acexmidlem2 5894 fo1st 6183 fo2nd 6184 iordsmo 6323 tfrlem7 6343 tfrexlem 6360 mapsnf1o2 6723 1domsn 6846 inresflem 7090 0ct 7137 infnninf 7153 infnninfOLD 7154 exmidonfinlem 7223 exmidaclem 7238 pw1on 7256 sucpw1nel3 7263 1pi 7345 prarloclemcalc 7532 ltsopr 7626 ltsosr 7794 cnm 7862 axicn 7893 axaddf 7898 axmulf 7899 nnindnn 7923 ltso 8066 negiso 8943 nnind 8966 0z 9295 dfuzi 9394 cnref1o 9682 elrpii 9688 xrltso 9828 0e0icopnf 10011 0e0iccpnf 10012 fz0to4untppr 10156 fldiv4p1lem1div2 10338 expcl2lemap 10566 expclzaplem 10578 expge0 10590 expge1 10591 xrnegiso 11305 fclim 11337 eff2 11723 reeff1 11743 ef01bndlem 11799 sin01bnd 11800 cos01bnd 11801 sin01gt0 11804 egt2lt3 11822 halfleoddlt 11934 2prm 12162 3prm 12163 1arith 12402 setsslnid 12567 xpsff1o 12828 isabli 13256 rngmgpf 13308 mgpf 13382 zringnzr 13918 fntopon 14001 istpsi 14016 ismeti 14323 tgqioo 14524 addcncntoplem 14528 divcnap 14532 abscncf 14549 recncf 14550 imcncf 14551 cjcncf 14552 dveflem 14664 reeff1o 14671 reefiso 14675 ioocosf1o 14752 lgslem2 14880 lgsfcl2 14885 lgsne0 14917 ex-fl 14955 bj-indint 15161 bj-omord 15190 012of 15224 2o01f 15225 0nninf 15232 peano4nninf 15234 taupi 15300 |
Copyright terms: Public domain | W3C validator |