Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp2d | GIF version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
3simp1d.1 | ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Ref | Expression |
---|---|
simp2d | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1d.1 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) | |
2 | simp2 967 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: simp2bi 982 erinxp 6471 resixp 6595 addcanprleml 7390 addcanprlemu 7391 ltmprr 7418 lelttrdi 8156 ixxdisj 9654 ixxss1 9655 ixxss2 9656 ixxss12 9657 iccgelb 9683 iccss2 9695 icodisj 9743 ioom 10006 flqdiv 10062 mulqaddmodid 10105 modsumfzodifsn 10137 addmodlteq 10139 immul 10619 sumtp 11151 crth 11827 phimullem 11828 ctiunct 11880 structn0fun 11899 strleund 11974 lmcl 12341 lmtopcnp 12346 xmeter 12532 tgqioo 12643 ivthinclemlopn 12710 ivthinclemuopn 12712 limcimolemlt 12729 limcresi 12731 limccnpcntop 12740 limccnp2lem 12741 limccnp2cntop 12742 cosordlem 12857 |
Copyright terms: Public domain | W3C validator |