![]() |
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 952 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | |
2 | 1 | adantr 272 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 930 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 932 |
This theorem is referenced by: fidifsnen 6693 ordiso2 6835 ctssdc 6912 addlocpr 7245 xltadd1 9500 hashun 10392 fimaxq 10414 xrmaxltsup 10866 dvdslegcd 11448 lcmledvds 11544 divgcdcoprm0 11575 rpexp 11624 iscnp4 12168 cnconst2 12183 blssps 12355 blss 12356 metcnp 12436 cdivcncfap 12499 |
Copyright terms: Public domain | W3C validator |