![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpll2 | Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 1001 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 276 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: fidceq 6868 fidifsnen 6869 en2eqpr 6906 iunfidisj 6944 ctssdc 7111 cauappcvgprlemlol 7645 caucvgprlemlol 7668 caucvgprprlemlol 7696 elfzonelfzo 10229 qbtwnre 10256 nn0ltexp2 10688 hashun 10784 xrmaxltsup 11265 subcn2 11318 prodmodclem2 11584 divalglemex 11926 divalglemeuneg 11927 dvdslegcd 11964 lcmledvds 12069 modprmn0modprm0 12255 qexpz 12349 iscnp4 13654 cnrest2 13672 blssps 13863 blss 13864 bdbl 13939 metcnp3 13947 addcncntoplem 13987 cdivcncfap 14023 lgsfcl2 14343 lgsdir 14372 lgsne0 14375 |
Copyright terms: Public domain | W3C validator |