![]() |
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 120 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simpld 112 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm5.62dc 945 3simpa 994 xoror 1379 anxordi 1400 sbidm 1851 reurex 2691 eqimss 3211 eldifi 3259 elinel1 3323 inss1 3357 sopo 4315 wefr 4360 ordtr 4380 opelxp1 4662 relop 4779 funmo 5233 funrel 5235 funinsn 5267 fnfun 5315 ffn 5367 f1f 5423 f1of1 5462 f1ofo 5470 isof1o 5811 eqopi 6176 1st2nd2 6179 reldmtpos 6257 swoer 6566 ecopover 6636 ecopoverg 6639 fnfi 6939 casef 7090 nninff 7124 lpowlpo 7169 dfplpq2 7356 enq0ref 7435 cauappcvgprlemopl 7648 cauappcvgprlemdisj 7653 caucvgprlemopl 7671 caucvgprlemdisj 7676 caucvgprprlemopl 7699 caucvgprprlemopu 7701 caucvgprprlemdisj 7704 peano1nnnn 7854 axrnegex 7881 ltxrlt 8026 1nn 8933 zre 9260 nnssz 9273 ixxss1 9907 ixxss2 9908 ixxss12 9909 iccss2 9947 rge0ssre 9980 elfzuz 10024 uzdisj 10096 nn0disj 10141 frecuzrdgtcl 10415 frecuzrdgfunlem 10422 modfsummodlemstep 11468 mertenslem2 11547 prmnn 12113 prmuz2 12134 oddpwdc 12177 sqpweven 12178 2sqpwodd 12179 phimullem 12228 hashgcdlem 12241 1arith 12368 ctinfom 12432 ctinf 12434 sgrpmgm 12820 mndsgrp 12830 grpmnd 12892 nsgsubg 13079 ablgrp 13108 cmnmnd 13119 crngring 13229 subrgring 13383 subrgrcl 13385 topontop 13702 tpstop 13723 cntop1 13889 cntop2 13890 hmeocn 13993 isxmet2d 14036 metxmet 14043 xmstps 14145 msxms 14146 xmsxmet 14148 msmet 14149 bdxmet 14189 ivthinclemlr 14303 ivthinclemur 14305 bj-indint 14871 bj-inf2vnlem2 14911 peano4nninf 14944 |
Copyright terms: Public domain | W3C validator |