![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simplbi | GIF version |
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
simplbi.1 | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
simplbi | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplbi.1 | . . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | |
2 | 1 | biimpi 119 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simpld 111 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.62dc 930 3simpa 979 xoror 1358 anxordi 1379 sbidm 1824 reurex 2647 eqimss 3156 eldifi 3203 elinel1 3267 inss1 3301 sopo 4243 wefr 4288 ordtr 4308 opelxp1 4581 relop 4697 funmo 5146 funrel 5148 funinsn 5180 fnfun 5228 ffn 5280 f1f 5336 f1of1 5374 f1ofo 5382 isof1o 5716 eqopi 6078 1st2nd2 6081 reldmtpos 6158 swoer 6465 ecopover 6535 ecopoverg 6538 fnfi 6833 casef 6981 dfplpq2 7186 enq0ref 7265 cauappcvgprlemopl 7478 cauappcvgprlemdisj 7483 caucvgprlemopl 7501 caucvgprlemdisj 7506 caucvgprprlemopl 7529 caucvgprprlemopu 7531 caucvgprprlemdisj 7534 peano1nnnn 7684 axrnegex 7711 ltxrlt 7854 1nn 8755 zre 9082 nnssz 9095 ixxss1 9717 ixxss2 9718 ixxss12 9719 iccss2 9757 rge0ssre 9790 elfzuz 9833 uzdisj 9904 nn0disj 9946 frecuzrdgtcl 10216 frecuzrdgfunlem 10223 modfsummodlemstep 11258 mertenslem2 11337 prmnn 11827 prmuz2 11847 oddpwdc 11888 sqpweven 11889 2sqpwodd 11890 phimullem 11937 hashgcdlem 11939 ctinfom 11977 ctinf 11979 topontop 12220 tpstop 12241 cntop1 12409 cntop2 12410 hmeocn 12513 isxmet2d 12556 metxmet 12563 xmstps 12665 msxms 12666 xmsxmet 12668 msmet 12669 bdxmet 12709 ivthinclemlr 12823 ivthinclemur 12825 bj-indint 13300 bj-inf2vnlem2 13340 nninff 13373 peano4nninf 13375 |
Copyright terms: Public domain | W3C validator |