![]() |
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 969 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | |
2 | 1 | adantr 272 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 945 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: frirrg 4232 fidceq 6716 fidifsnen 6717 en2eqpr 6754 iunfidisj 6786 ordiso2 6872 addlocpr 7289 aptiprlemu 7393 xltadd1 9549 xlesubadd 9556 icoshftf1o 9664 fztri3or 9709 elfzonelfzo 9897 exp3val 10185 hashun 10441 subcn2 10969 divalglemeuneg 11465 dvdslegcd 11498 lcmledvds 11594 rpdvds 11623 cncongr2 11628 iuncld 12124 iscnp4 12226 cnpnei 12227 cnconst2 12241 cnpdis 12250 txcn 12283 blssps 12413 blss 12414 metcnp3 12497 metcnp 12498 |
Copyright terms: Public domain | W3C validator |