| 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 1003 |
. 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 983 |
| This theorem is referenced by: fidifsnen 6967 ordiso2 7137 ctssdc 7215 addlocpr 7649 xltadd1 9998 nn0ltexp2 10854 hashun 10950 fimaxq 10972 xrmaxltsup 11569 dvdslegcd 12285 lcmledvds 12392 divgcdcoprm0 12423 rpexp 12475 qexpz 12675 dfgrp3mlem 13430 rhmdvdsr 13937 rnglidlmcl 14242 iscnp4 14690 cnconst2 14705 blssps 14899 blss 14900 metcnp 14984 addcncntoplem 15033 cdivcncfap 15076 lgsfvalg 15482 lgsmod 15503 lgsdir 15512 lgsne0 15515 |
| Copyright terms: Public domain | W3C validator |