![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpll2 | GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll2 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 950 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | |
2 | 1 | adantr 271 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 927 |
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 929 |
This theorem is referenced by: fidceq 6665 fidifsnen 6666 en2eqpr 6703 iunfidisj 6735 cauappcvgprlemlol 7303 caucvgprlemlol 7326 caucvgprprlemlol 7354 elfzonelfzo 9790 qbtwnre 9817 hashun 10344 xrmaxltsup 10817 subcn2 10870 divalglemex 11364 divalglemeuneg 11365 dvdslegcd 11398 lcmledvds 11494 iscnp4 12084 cnrest2 12102 blssps 12228 blss 12229 bdbl 12304 metcnp3 12308 |
Copyright terms: Public domain | W3C validator |