![]() |
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 964 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 945 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: simp1bi 979 erinxp 6457 addcanprleml 7370 addcanprlemu 7371 ltmprr 7398 lelttrdi 8107 ixxdisj 9579 ixxss1 9580 ixxss2 9581 ixxss12 9582 iccss2 9620 iocssre 9629 icossre 9630 iccssre 9631 icodisj 9668 iccf1o 9680 fzen 9716 ioom 9931 intfracq 9986 flqdiv 9987 mulqaddmodid 10030 modsumfzodifsn 10062 addmodlteq 10064 remul 10537 sumtp 11075 crth 11745 phimullem 11746 ctiunct 11796 strsetsid 11835 strleund 11890 lmfpm 12254 lmff 12260 lmtopcnp 12261 xmeter 12425 tgqioo 12533 limcimolemlt 12589 limcresi 12591 |
Copyright terms: Public domain | W3C validator |