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 914 3simpa 963 xoror 1342 anxordi 1363 sbidm 1807 reurex 2621 eqimss 3121 eldifi 3168 elinel1 3232 inss1 3266 sopo 4205 wefr 4250 ordtr 4270 opelxp1 4543 relop 4659 funmo 5108 funrel 5110 funinsn 5142 fnfun 5190 ffn 5242 f1f 5298 f1of1 5334 f1ofo 5342 isof1o 5676 eqopi 6038 1st2nd2 6041 reldmtpos 6118 swoer 6425 ecopover 6495 ecopoverg 6498 fnfi 6793 casef 6941 dfplpq2 7130 enq0ref 7209 cauappcvgprlemopl 7422 cauappcvgprlemdisj 7427 caucvgprlemopl 7445 caucvgprlemdisj 7450 caucvgprprlemopl 7473 caucvgprprlemopu 7475 caucvgprprlemdisj 7478 peano1nnnn 7628 axrnegex 7655 ltxrlt 7798 1nn 8699 zre 9026 nnssz 9039 ixxss1 9655 ixxss2 9656 ixxss12 9657 iccss2 9695 rge0ssre 9728 elfzuz 9770 uzdisj 9841 nn0disj 9883 frecuzrdgtcl 10153 frecuzrdgfunlem 10160 modfsummodlemstep 11194 mertenslem2 11273 prmnn 11718 prmuz2 11738 oddpwdc 11779 sqpweven 11780 2sqpwodd 11781 phimullem 11828 hashgcdlem 11830 ctinfom 11868 ctinf 11870 topontop 12108 tpstop 12129 cntop1 12297 cntop2 12298 hmeocn 12401 isxmet2d 12444 metxmet 12451 xmstps 12553 msxms 12554 xmsxmet 12556 msmet 12557 bdxmet 12597 ivthinclemlr 12711 ivthinclemur 12713 bj-indint 13056 bj-inf2vnlem2 13096 nninff 13125 peano4nninf 13127 |
Copyright terms: Public domain | W3C validator |