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 995 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | |
2 | 1 | adantr 274 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 973 |
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 975 |
This theorem is referenced by: fidifsnen 6846 ordiso2 7010 ctssdc 7088 addlocpr 7491 xltadd1 9826 nn0ltexp2 10637 hashun 10733 fimaxq 10755 xrmaxltsup 11214 dvdslegcd 11912 lcmledvds 12017 divgcdcoprm0 12048 rpexp 12100 qexpz 12297 iscnp4 12977 cnconst2 12992 blssps 13186 blss 13187 metcnp 13271 addcncntoplem 13310 cdivcncfap 13346 lgsfvalg 13665 lgsmod 13686 lgsdir 13695 lgsne0 13698 |
Copyright terms: Public domain | W3C validator |