![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpll1 | GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll1 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1002 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | |
2 | 1 | adantr 276 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: fidifsnen 6899 ordiso2 7065 ctssdc 7143 addlocpr 7566 xltadd1 9908 nn0ltexp2 10724 hashun 10820 fimaxq 10842 xrmaxltsup 11301 dvdslegcd 12000 lcmledvds 12105 divgcdcoprm0 12136 rpexp 12188 qexpz 12387 dfgrp3mlem 13057 rhmdvdsr 13542 rnglidlmcl 13813 iscnp4 14195 cnconst2 14210 blssps 14404 blss 14405 metcnp 14489 addcncntoplem 14528 cdivcncfap 14564 lgsfvalg 14884 lgsmod 14905 lgsdir 14914 lgsne0 14917 |
Copyright terms: Public domain | W3C validator |