![]() |
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 986 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 274 |
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 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: fidceq 6771 fidifsnen 6772 en2eqpr 6809 iunfidisj 6842 ctssdc 7006 cauappcvgprlemlol 7479 caucvgprlemlol 7502 caucvgprprlemlol 7530 elfzonelfzo 10038 qbtwnre 10065 hashun 10583 xrmaxltsup 11059 subcn2 11112 prodmodclem2 11378 divalglemex 11655 divalglemeuneg 11656 dvdslegcd 11689 lcmledvds 11787 iscnp4 12426 cnrest2 12444 blssps 12635 blss 12636 bdbl 12711 metcnp3 12719 addcncntoplem 12759 cdivcncfap 12795 |
Copyright terms: Public domain | W3C validator |