![]() |
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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.62dc 892 3simpa 941 xoror 1316 anxordi 1337 sbidm 1780 reurex 2581 eqimss 3079 eldifi 3123 elinel1 3187 inss1 3221 sopo 4149 wefr 4194 ordtr 4214 opelxp1 4485 relop 4599 funmo 5043 funrel 5045 funinsn 5076 fnfun 5124 ffn 5174 f1f 5229 f1of1 5265 f1ofo 5273 isof1o 5600 eqopi 5956 1st2nd2 5959 reldmtpos 6032 swoer 6334 ecopover 6404 ecopoverg 6407 fnfi 6700 casef 6833 dfplpq2 6974 enq0ref 7053 cauappcvgprlemopl 7266 cauappcvgprlemdisj 7271 caucvgprlemopl 7289 caucvgprlemdisj 7294 caucvgprprlemopl 7317 caucvgprprlemopu 7319 caucvgprprlemdisj 7322 peano1nnnn 7450 axrnegex 7475 ltxrlt 7613 1nn 8494 zre 8815 nnssz 8828 ixxss1 9383 ixxss2 9384 ixxss12 9385 iccss2 9423 rge0ssre 9456 elfzuz 9497 uzdisj 9568 nn0disj 9610 frecuzrdgtcl 9880 frecuzrdgfunlem 9887 modfsummodlemstep 10912 mertenslem2 10991 prmnn 11431 prmuz2 11451 oddpwdc 11491 sqpweven 11492 2sqpwodd 11493 phimullem 11540 hashgcdlem 11542 topontop 11774 tpstop 11794 bj-indint 12099 bj-inf2vnlem2 12139 nninff 12166 peano4nninf 12168 |
Copyright terms: Public domain | W3C validator |