Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp3d | GIF version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
3simp1d.1 | ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Ref | Expression |
---|---|
simp3d | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1d.1 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
2 | simp3 983 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: simp3bi 998 erinxp 6503 resixp 6627 addcanprleml 7422 addcanprlemu 7423 ltmprr 7450 lelttrdi 8188 ixxdisj 9686 ixxss1 9687 ixxss2 9688 ixxss12 9689 iccsupr 9749 icodisj 9775 ioom 10038 intfracq 10093 flqdiv 10094 mulqaddmodid 10137 modsumfzodifsn 10169 cjmul 10657 sumtp 11183 crth 11900 ennnfonelemim 11937 ctiunct 11953 strsetsid 11992 strleund 12047 lmcvg 12386 lmff 12418 lmtopcnp 12419 xmeter 12605 xmetresbl 12609 tgqioo 12716 ivthinclemlopn 12783 ivthinclemuopn 12785 limccl 12797 limcdifap 12800 limcresi 12804 limccnpcntop 12813 limccnp2lem 12814 limccnp2cntop 12815 limccoap 12816 cosordlem 12930 |
Copyright terms: Public domain | W3C validator |