![]() |
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 999 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 |
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 982 |
This theorem is referenced by: simp1bi 1014 erinxp 6636 exmidapne 7290 addcanprleml 7644 addcanprlemu 7645 ltmprr 7672 lelttrdi 8414 ixxdisj 9935 ixxss1 9936 ixxss2 9937 ixxss12 9938 iccss2 9976 iocssre 9985 icossre 9986 iccssre 9987 icodisj 10024 iccf1o 10036 fzen 10075 ioom 10293 intfracq 10353 flqdiv 10354 mulqaddmodid 10397 modsumfzodifsn 10429 addmodlteq 10431 remul 10916 sumtp 11457 crth 12259 phimullem 12260 eulerthlem1 12262 eulerthlemfi 12263 eulerthlemrprm 12264 eulerthlema 12265 eulerthlemh 12266 eulerthlemth 12267 ctiunct 12494 strsetsid 12548 strleund 12618 strext 12620 mhmf 12932 submss 12943 eqger 13180 eqgcpbl 13184 lmodvscl 13638 lssssg 13693 rnglidlmsgrp 13830 2idlcpblrng 13855 lmfpm 14220 lmff 14226 lmtopcnp 14227 xmeter 14413 tgqioo 14524 ivthinclemlopn 14591 ivthinclemuopn 14593 limcimolemlt 14610 limcresi 14612 cosordlem 14747 relogbval 14846 relogbzcl 14847 nnlogbexp 14854 |
Copyright terms: Public domain | W3C validator |