![]() |
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 113 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
3 | 2 | simpld 105 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm5.62dc 852 3simpa 901 xoror 1270 anxordi 1291 sbidm 1731 reurex 2523 eqimss 2997 pssss 3039 eldifi 3066 inss1 3157 sopo 4050 wefr 4095 ordtr 4115 opelxp1 4377 relop 4486 funmo 4917 funrel 4919 fnfun 4996 ffn 5046 f1f 5092 f1of1 5125 f1ofo 5133 isof1o 5447 eqopi 5798 1st2nd2 5801 reldmtpos 5868 swoer 6134 ecopover 6204 ecopoverg 6207 dfplpq2 6452 enq0ref 6531 cauappcvgprlemopl 6744 cauappcvgprlemdisj 6749 caucvgprlemopl 6767 caucvgprlemdisj 6772 caucvgprprlemopl 6795 caucvgprprlemopu 6797 caucvgprprlemdisj 6800 peano1nnnn 6928 axrnegex 6953 ltxrlt 7085 1nn 7925 zre 8249 nnssz 8262 ixxss1 8773 ixxss2 8774 ixxss12 8775 iccss2 8813 rge0ssre 8846 elfzuz 8886 uzdisj 8955 nn0disj 8995 frecuzrdgfn 9198 bj-indint 10055 bj-inf2vnlem2 10096 |
Copyright terms: Public domain | W3C validator |