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 984 | . 2 | |
2 | 1 | adantr 274 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
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 964 |
This theorem is referenced by: fidifsnen 6764 ordiso2 6920 ctssdc 6998 addlocpr 7344 xltadd1 9659 hashun 10551 fimaxq 10573 xrmaxltsup 11027 dvdslegcd 11653 lcmledvds 11751 divgcdcoprm0 11782 rpexp 11831 iscnp4 12387 cnconst2 12402 blssps 12596 blss 12597 metcnp 12681 addcncntoplem 12720 cdivcncfap 12756 |
Copyright terms: Public domain | W3C validator |