![]() |
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 941 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: simp3bi 956 erinxp 6296 addcanprleml 7076 addcanprlemu 7077 ltmprr 7104 lelttrdi 7807 ixxdisj 9216 ixxss1 9217 ixxss2 9218 ixxss12 9219 iccsupr 9279 icodisj 9304 ioom 9561 intfracq 9616 flqdiv 9617 mulqaddmodid 9660 modsumfzodifsn 9692 cjmul 10146 crth 10980 |
Copyright terms: Public domain | W3C validator |