![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpll1 | Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpll1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1002 |
. 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 982 |
This theorem is referenced by: fidifsnen 6898 ordiso2 7064 ctssdc 7142 addlocpr 7565 xltadd1 9906 nn0ltexp2 10721 hashun 10817 fimaxq 10839 xrmaxltsup 11298 dvdslegcd 11997 lcmledvds 12102 divgcdcoprm0 12133 rpexp 12185 qexpz 12384 dfgrp3mlem 13042 rhmdvdsr 13525 rnglidlmcl 13796 iscnp4 14175 cnconst2 14190 blssps 14384 blss 14385 metcnp 14469 addcncntoplem 14508 cdivcncfap 14544 lgsfvalg 14864 lgsmod 14885 lgsdir 14894 lgsne0 14897 |
Copyright terms: Public domain | W3C validator |