![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp1d | GIF version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
3simp1d.1 | ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Ref | Expression |
---|---|
simp1d | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1d.1 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
2 | simp1 997 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: simp1bi 1012 erinxp 6602 addcanprleml 7591 addcanprlemu 7592 ltmprr 7619 lelttrdi 8360 ixxdisj 9877 ixxss1 9878 ixxss2 9879 ixxss12 9880 iccss2 9918 iocssre 9927 icossre 9928 iccssre 9929 icodisj 9966 iccf1o 9978 fzen 10016 ioom 10234 intfracq 10293 flqdiv 10294 mulqaddmodid 10337 modsumfzodifsn 10369 addmodlteq 10371 remul 10852 sumtp 11393 crth 12194 phimullem 12195 eulerthlem1 12197 eulerthlemfi 12198 eulerthlemrprm 12199 eulerthlema 12200 eulerthlemh 12201 eulerthlemth 12202 ctiunct 12411 strsetsid 12465 strleund 12531 mhmf 12733 submss 12744 lmfpm 13376 lmff 13382 lmtopcnp 13383 xmeter 13569 tgqioo 13680 ivthinclemlopn 13747 ivthinclemuopn 13749 limcimolemlt 13766 limcresi 13768 cosordlem 13903 relogbval 14002 relogbzcl 14003 nnlogbexp 14010 |
Copyright terms: Public domain | W3C validator |