![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpll3 | GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll3 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 1004 | . 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 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: frirrg 4368 fidceq 6896 fidifsnen 6897 en2eqpr 6934 iunfidisj 6974 ordiso2 7063 addlocpr 7564 aptiprlemu 7668 xltadd1 9905 xlesubadd 9912 icoshftf1o 10020 fztri3or 10068 elfzonelfzo 10259 exp3val 10552 nn0ltexp2 10720 hashun 10816 subcn2 11350 divalglemeuneg 11959 dvdslegcd 11996 lcmledvds 12101 rpdvds 12130 cncongr2 12135 qexpz 12383 iuncld 14067 iscnp4 14170 cnpnei 14171 cnconst2 14185 cnpdis 14194 txcn 14227 blssps 14379 blss 14380 metcnp3 14463 metcnp 14464 lgsfcl2 14860 lgsdir 14889 lgsne0 14892 |
Copyright terms: Public domain | W3C validator |