![]() |
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 851 3simpa 900 anxordi 1288 sbidm 1728 reurex 2517 eqimss 2991 pssss 3033 eldifi 3060 inss1 3151 sopo 4041 ordtr 4081 opelxp1 4320 relop 4429 funmo 4860 funrel 4862 fnfun 4939 ffn 4989 f1f 5035 f1of1 5068 f1ofo 5076 isof1o 5390 eqopi 5740 1st2nd2 5743 reldmtpos 5809 swoer 6070 ecopover 6140 ecopoverg 6143 dfplpq2 6338 enq0ref 6416 cauappcvgprlemopl 6618 cauappcvgprlemdisj 6623 caucvgprlemopl 6640 caucvgprlemdisj 6645 axrnegex 6763 ltxrlt 6882 1nn 7706 zre 8025 nnssz 8038 ixxss1 8543 ixxss2 8544 ixxss12 8545 iccss2 8583 rge0ssre 8616 elfzuz 8656 uzdisj 8725 nn0disj 8765 frecuzrdgfn 8879 bj-indint 9390 bj-inf2vnlem2 9431 |
Copyright terms: Public domain | W3C validator |