| 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 6966 ordiso2 7136 ctssdc 7214 addlocpr 7648 xltadd1 9997 nn0ltexp2 10852 hashun 10948 fimaxq 10970 xrmaxltsup 11540 dvdslegcd 12256 lcmledvds 12363 divgcdcoprm0 12394 rpexp 12446 qexpz 12646 dfgrp3mlem 13401 rhmdvdsr 13908 rnglidlmcl 14213 iscnp4 14661 cnconst2 14676 blssps 14870 blss 14871 metcnp 14955 addcncntoplem 15004 cdivcncfap 15047 lgsfvalg 15453 lgsmod 15474 lgsdir 15483 lgsne0 15486 |
| Copyright terms: Public domain | W3C validator |