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 986 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | |
2 | 1 | adantr 274 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 963 |
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 965 |
This theorem is referenced by: fidceq 6816 fidifsnen 6817 en2eqpr 6854 iunfidisj 6892 ctssdc 7059 cauappcvgprlemlol 7569 caucvgprlemlol 7592 caucvgprprlemlol 7620 elfzonelfzo 10138 qbtwnre 10165 nn0ltexp2 10595 hashun 10690 xrmaxltsup 11166 subcn2 11219 prodmodclem2 11485 divalglemex 11825 divalglemeuneg 11826 dvdslegcd 11863 lcmledvds 11962 modprmn0modprm0 12146 iscnp4 12688 cnrest2 12706 blssps 12897 blss 12898 bdbl 12973 metcnp3 12981 addcncntoplem 13021 cdivcncfap 13057 |
Copyright terms: Public domain | W3C validator |