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 934 3simpa 983 xoror 1368 anxordi 1389 sbidm 1838 reurex 2677 eqimss 3194 eldifi 3242 elinel1 3306 inss1 3340 sopo 4288 wefr 4333 ordtr 4353 opelxp1 4635 relop 4751 funmo 5200 funrel 5202 funinsn 5234 fnfun 5282 ffn 5334 f1f 5390 f1of1 5428 f1ofo 5436 isof1o 5772 eqopi 6135 1st2nd2 6138 reldmtpos 6215 swoer 6523 ecopover 6593 ecopoverg 6596 fnfi 6896 casef 7047 nninff 7081 lpowlpo 7126 dfplpq2 7289 enq0ref 7368 cauappcvgprlemopl 7581 cauappcvgprlemdisj 7586 caucvgprlemopl 7604 caucvgprlemdisj 7609 caucvgprprlemopl 7632 caucvgprprlemopu 7634 caucvgprprlemdisj 7637 peano1nnnn 7787 axrnegex 7814 ltxrlt 7958 1nn 8862 zre 9189 nnssz 9202 ixxss1 9834 ixxss2 9835 ixxss12 9836 iccss2 9874 rge0ssre 9907 elfzuz 9950 uzdisj 10022 nn0disj 10067 frecuzrdgtcl 10341 frecuzrdgfunlem 10348 modfsummodlemstep 11392 mertenslem2 11471 prmnn 12036 prmuz2 12057 oddpwdc 12100 sqpweven 12101 2sqpwodd 12102 phimullem 12151 hashgcdlem 12164 1arith 12291 ctinfom 12355 ctinf 12357 topontop 12610 tpstop 12631 cntop1 12799 cntop2 12800 hmeocn 12903 isxmet2d 12946 metxmet 12953 xmstps 13055 msxms 13056 xmsxmet 13058 msmet 13059 bdxmet 13099 ivthinclemlr 13213 ivthinclemur 13215 bj-indint 13706 bj-inf2vnlem2 13746 peano4nninf 13779 |
Copyright terms: Public domain | W3C validator |